Step | Hyp | Ref
| Expression |
1 | | df-reu 2903 |
. . 3
⊢
(∃!𝑥 ∈
{𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ∃!𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
2 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑦 ∈ {𝐴, 𝐵, 𝐶})) |
3 | | preq1 4212 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → {𝑥, 𝐴} = {𝑦, 𝐴}) |
4 | | preq1 4212 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → {𝑥, 𝐵} = {𝑦, 𝐵}) |
5 | 3, 4 | preq12d 4220 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝑦, 𝐴}, {𝑦, 𝐵}}) |
6 | 5 | sseq1d 3595 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) |
7 | 2, 6 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ↔ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸))) |
8 | 7 | eu4 2506 |
. . . 4
⊢
(∃!𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ↔ (∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦))) |
9 | | frgra3vlem1 26527 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦)) |
10 | 9 | biantrud 527 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ↔ (∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦)))) |
11 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
12 | 11 | eltp 4177 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)) |
13 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → {𝑥, 𝐴} = {𝐴, 𝐴}) |
14 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵}) |
15 | 13, 14 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐴, 𝐴}, {𝐴, 𝐵}}) |
16 | 15 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸)) |
17 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐴, 𝐴} ∈ V |
18 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐴, 𝐵} ∈ V |
19 | 17, 18 | prss 4291 |
. . . . . . . . . . . . 13
⊢ (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸) |
20 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴 ≠ 𝐴) |
21 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐴) |
22 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = 𝐴 |
23 | 22 | pm2.24i 145 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝐴 = 𝐴 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
24 | 21, 23 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ≠ 𝐴 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
25 | 20, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
26 | 25 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
28 | 27 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
30 | 19, 29 | sylbir 224 |
. . . . . . . . . . . 12
⊢ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
31 | 16, 30 | syl6bi 242 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
32 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → {𝑥, 𝐴} = {𝐵, 𝐴}) |
33 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → {𝑥, 𝐵} = {𝐵, 𝐵}) |
34 | 32, 33 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐵, 𝐴}, {𝐵, 𝐵}}) |
35 | 34 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸)) |
36 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐵, 𝐴} ∈ V |
37 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐵, 𝐵} ∈ V |
38 | 36, 37 | prss 4291 |
. . . . . . . . . . . . 13
⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸) |
39 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → 𝐵 ≠ 𝐵) |
40 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐵) |
41 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 = 𝐵 |
42 | 41 | pm2.24i 145 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝐵 = 𝐵 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
43 | 40, 42 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ≠ 𝐵 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
44 | 39, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
45 | 44 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐵, 𝐵} ∈ ran 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐵, 𝐵} ∈ ran 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ({𝐵, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
49 | 38, 48 | sylbir 224 |
. . . . . . . . . . . 12
⊢ ({{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
50 | 35, 49 | syl6bi 242 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
51 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐶 → {𝑥, 𝐴} = {𝐶, 𝐴}) |
52 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐶 → {𝑥, 𝐵} = {𝐶, 𝐵}) |
53 | 51, 52 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐶, 𝐴}, {𝐶, 𝐵}}) |
54 | 53 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸)) |
55 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐶, 𝐴} ∈ V |
56 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐶, 𝐵} ∈ V |
57 | 55, 56 | prss 4291 |
. . . . . . . . . . . . 13
⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸) |
58 | | ax-1 6 |
. . . . . . . . . . . . 13
⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
59 | 57, 58 | sylbir 224 |
. . . . . . . . . . . 12
⊢ ({{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
60 | 54, 59 | syl6bi 242 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
61 | 31, 50, 60 | 3jaoi 1383 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
62 | 12, 61 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
63 | 62 | imp 444 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
64 | 63 | com12 32 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
65 | 64 | exlimdv 1848 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
66 | | prssi 4293 |
. . . . . . . . . . 11
⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) → {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸) |
67 | 66 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) → {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸) |
68 | 67 | 3mix3d 1231 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) → ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸)) |
69 | 16, 35, 54 | rextpg 4184 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸))) |
70 | 69 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐶, 𝐴}, {𝐶, 𝐵}} ⊆ ran 𝐸))) |
71 | 68, 70 | mpbird 246 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) → ∃𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) |
72 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
73 | 71, 72 | sylib 207 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) → ∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
74 | 73 | ex 449 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) → ∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸))) |
75 | 65, 74 | impbid 201 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
76 | 10, 75 | bitr3d 269 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((∃𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦)) ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
77 | 8, 76 | syl5bb 271 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥(𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
78 | 1, 77 | syl5bb 271 |
. 2
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
79 | 78 | ex 449 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |