Proof of Theorem nb3grapr
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
2 | | prcom 4211 |
. . . . . . . . . 10
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} |
3 | 2 | eleq1i 2679 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸) |
4 | | prcom 4211 |
. . . . . . . . . 10
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
5 | 4 | eleq1i 2679 |
. . . . . . . . 9
⊢ ({𝐵, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐵} ∈ ran 𝐸) |
6 | | prcom 4211 |
. . . . . . . . . 10
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
7 | 6 | eleq1i 2679 |
. . . . . . . . 9
⊢ ({𝐶, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸) |
8 | 3, 5, 7 | 3anbi123i 1244 |
. . . . . . . 8
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) |
9 | | 3anrot 1036 |
. . . . . . . 8
⊢ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) |
10 | 8, 9 | bitr4i 266 |
. . . . . . 7
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
12 | 1, 11 | biadan2 672 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
13 | | an6 1400 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
14 | 12, 13 | bitri 263 |
. . . 4
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
15 | 14 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
16 | | nb3graprlem1 25980 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) |
17 | | 3anrot 1036 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋)) |
18 | 17 | biimpi 205 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋)) |
19 | | tprot 4228 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
20 | 19 | eqeq2i 2622 |
. . . . . . . 8
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐶, 𝐴}) |
21 | 20 | biimpi 205 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐶, 𝐴}) |
22 | 21 | anim1i 590 |
. . . . . 6
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝑉 USGrph 𝐸)) |
23 | | nb3graprlem1 25980 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸))) |
24 | 18, 22, 23 | syl2an 493 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸))) |
25 | | 3anrot 1036 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
26 | 25 | biimpri 217 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
27 | | tprot 4228 |
. . . . . . . . . 10
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
28 | 27 | eqcomi 2619 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} |
29 | 28 | eqeq2i 2622 |
. . . . . . . 8
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵}) |
30 | 29 | biimpi 205 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵}) |
31 | 30 | anim1i 590 |
. . . . . 6
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) |
32 | | nb3graprlem1 25980 |
. . . . . 6
⊢ (((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
33 | 26, 31, 32 | syl2an 493 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
34 | 16, 24, 33 | 3anbi123d 1391 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
35 | 34 | 3adant3 1074 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
36 | | nb3graprlem2 25981 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧})) |
37 | 20 | anbi1i 727 |
. . . . 5
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ↔ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝑉 USGrph 𝐸)) |
38 | | necom 2835 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
39 | | necom 2835 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴) |
40 | | biid 250 |
. . . . . . 7
⊢ (𝐵 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
41 | 38, 39, 40 | 3anbi123i 1244 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) |
42 | | 3anrot 1036 |
. . . . . 6
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) |
43 | 41, 42 | bitr4i 266 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) |
44 | | nb3graprlem2 25981 |
. . . . 5
⊢ (((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝑉 USGrph 𝐸) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧})) |
45 | 17, 37, 43, 44 | syl3anb 1361 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧})) |
46 | | id 22 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐵, 𝐶}) |
47 | 46, 28 | syl6eq 2660 |
. . . . . 6
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵}) |
48 | 47 | anim1i 590 |
. . . . 5
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) |
49 | | 3anrot 1036 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵)) |
50 | | necom 2835 |
. . . . . . . 8
⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵) |
51 | | biid 250 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐵) |
52 | 39, 50, 51 | 3anbi123i 1244 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
53 | 49, 52 | bitri 263 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
54 | 53 | biimpi 205 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
55 | | nb3graprlem2 25981 |
. . . . 5
⊢ (((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧})) |
56 | 26, 48, 54, 55 | syl3an 1360 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧})) |
57 | 36, 45, 56 | 3anbi123d 1391 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐶, 𝐴} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}) ↔ (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧}))) |
58 | 15, 35, 57 | 3bitr2d 295 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧}))) |
59 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝐴)) |
60 | 59 | eqeq1d 2612 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧})) |
61 | 60 | 2rexbidv 3039 |
. . . 4
⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧})) |
62 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝐵)) |
63 | 62 | eqeq1d 2612 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧})) |
64 | 63 | 2rexbidv 3039 |
. . . 4
⊢ (𝑥 = 𝐵 → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧})) |
65 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝐶)) |
66 | 65 | eqeq1d 2612 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧})) |
67 | 66 | 2rexbidv 3039 |
. . . 4
⊢ (𝑥 = 𝐶 → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧})) |
68 | 61, 64, 67 | raltpg 4183 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧}))) |
69 | 68 | 3ad2ant1 1075 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝑦, 𝑧} ∧ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝑦, 𝑧}))) |
70 | | raleq 3115 |
. . . . 5
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∀𝑥 ∈ {𝐴, 𝐵, 𝐶}∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧})) |
71 | 70 | bicomd 212 |
. . . 4
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧})) |
72 | 71 | adantr 480 |
. . 3
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧})) |
73 | 72 | 3ad2ant2 1076 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧} ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧})) |
74 | 58, 69, 73 | 3bitr2d 295 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(〈𝑉, 𝐸〉 Neighbors 𝑥) = {𝑦, 𝑧})) |