Proof of Theorem wetriext
Step | Hyp | Ref
| Expression |
1 | | wetriext.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
2 | | wetriext.ext |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 (𝑧𝑅𝐵 ↔ 𝑧𝑅𝐶)) |
3 | | breq1 3788 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑧𝑅𝐵 ↔ 𝐵𝑅𝐵)) |
4 | | breq1 3788 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑧𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
5 | 3, 4 | bibi12d 233 |
. . . . . 6
⊢ (𝑧 = 𝐵 → ((𝑧𝑅𝐵 ↔ 𝑧𝑅𝐶) ↔ (𝐵𝑅𝐵 ↔ 𝐵𝑅𝐶))) |
6 | 5 | rspcv 2697 |
. . . . 5
⊢ (𝐵 ∈ 𝐴 → (∀𝑧 ∈ 𝐴 (𝑧𝑅𝐵 ↔ 𝑧𝑅𝐶) → (𝐵𝑅𝐵 ↔ 𝐵𝑅𝐶))) |
7 | 1, 2, 6 | sylc 61 |
. . . 4
⊢ (𝜑 → (𝐵𝑅𝐵 ↔ 𝐵𝑅𝐶)) |
8 | 7 | biimpar 291 |
. . 3
⊢ ((𝜑 ∧ 𝐵𝑅𝐶) → 𝐵𝑅𝐵) |
9 | | wetriext.we |
. . . . . 6
⊢ (𝜑 → 𝑅 We 𝐴) |
10 | | wefr 4113 |
. . . . . 6
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
11 | 9, 10 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑅 Fr 𝐴) |
12 | | wetriext.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
13 | | frirrg 4105 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
14 | 11, 12, 1, 13 | syl3anc 1169 |
. . . 4
⊢ (𝜑 → ¬ 𝐵𝑅𝐵) |
15 | 14 | adantr 270 |
. . 3
⊢ ((𝜑 ∧ 𝐵𝑅𝐶) → ¬ 𝐵𝑅𝐵) |
16 | 8, 15 | pm2.21dd 582 |
. 2
⊢ ((𝜑 ∧ 𝐵𝑅𝐶) → 𝐵 = 𝐶) |
17 | | simpr 108 |
. 2
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶) |
18 | | wetriext.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
19 | | breq1 3788 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑧𝑅𝐵 ↔ 𝐶𝑅𝐵)) |
20 | | breq1 3788 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑧𝑅𝐶 ↔ 𝐶𝑅𝐶)) |
21 | 19, 20 | bibi12d 233 |
. . . . . 6
⊢ (𝑧 = 𝐶 → ((𝑧𝑅𝐵 ↔ 𝑧𝑅𝐶) ↔ (𝐶𝑅𝐵 ↔ 𝐶𝑅𝐶))) |
22 | 21 | rspcv 2697 |
. . . . 5
⊢ (𝐶 ∈ 𝐴 → (∀𝑧 ∈ 𝐴 (𝑧𝑅𝐵 ↔ 𝑧𝑅𝐶) → (𝐶𝑅𝐵 ↔ 𝐶𝑅𝐶))) |
23 | 18, 2, 22 | sylc 61 |
. . . 4
⊢ (𝜑 → (𝐶𝑅𝐵 ↔ 𝐶𝑅𝐶)) |
24 | 23 | biimpa 290 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅𝐵) → 𝐶𝑅𝐶) |
25 | | frirrg 4105 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶𝑅𝐶) |
26 | 11, 12, 18, 25 | syl3anc 1169 |
. . . 4
⊢ (𝜑 → ¬ 𝐶𝑅𝐶) |
27 | 26 | adantr 270 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅𝐵) → ¬ 𝐶𝑅𝐶) |
28 | 24, 27 | pm2.21dd 582 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅𝐵) → 𝐵 = 𝐶) |
29 | | wetriext.tri |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)) |
30 | | breq1 3788 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (𝑎𝑅𝑏 ↔ 𝐵𝑅𝑏)) |
31 | | eqeq1 2087 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (𝑎 = 𝑏 ↔ 𝐵 = 𝑏)) |
32 | | breq2 3789 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (𝑏𝑅𝑎 ↔ 𝑏𝑅𝐵)) |
33 | 30, 31, 32 | 3orbi123d 1242 |
. . . . 5
⊢ (𝑎 = 𝐵 → ((𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ (𝐵𝑅𝑏 ∨ 𝐵 = 𝑏 ∨ 𝑏𝑅𝐵))) |
34 | | breq2 3789 |
. . . . . 6
⊢ (𝑏 = 𝐶 → (𝐵𝑅𝑏 ↔ 𝐵𝑅𝐶)) |
35 | | eqeq2 2090 |
. . . . . 6
⊢ (𝑏 = 𝐶 → (𝐵 = 𝑏 ↔ 𝐵 = 𝐶)) |
36 | | breq1 3788 |
. . . . . 6
⊢ (𝑏 = 𝐶 → (𝑏𝑅𝐵 ↔ 𝐶𝑅𝐵)) |
37 | 34, 35, 36 | 3orbi123d 1242 |
. . . . 5
⊢ (𝑏 = 𝐶 → ((𝐵𝑅𝑏 ∨ 𝐵 = 𝑏 ∨ 𝑏𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
38 | 33, 37 | rspc2v 2713 |
. . . 4
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
39 | 1, 18, 38 | syl2anc 403 |
. . 3
⊢ (𝜑 → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
40 | 29, 39 | mpd 13 |
. 2
⊢ (𝜑 → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) |
41 | 16, 17, 28, 40 | mpjao3dan 1238 |
1
⊢ (𝜑 → 𝐵 = 𝐶) |