Proof of Theorem nb3gra2nb
Step | Hyp | Ref
| Expression |
1 | | prcom 4211 |
. . . . . . . . 9
⊢ {𝐴, 𝐶} = {𝐶, 𝐴} |
2 | 1 | eleq1i 2679 |
. . . . . . . 8
⊢ ({𝐴, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐴} ∈ ran 𝐸) |
3 | 2 | biimpi 205 |
. . . . . . 7
⊢ ({𝐴, 𝐶} ∈ ran 𝐸 → {𝐶, 𝐴} ∈ ran 𝐸) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) → {𝐶, 𝐴} ∈ ran 𝐸) |
5 | | prcom 4211 |
. . . . . . . . 9
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
6 | 5 | eleq1i 2679 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐵} ∈ ran 𝐸) |
7 | 6 | biimpi 205 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ ran 𝐸 → {𝐶, 𝐵} ∈ ran 𝐸) |
8 | 7 | adantl 481 |
. . . . . 6
⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → {𝐶, 𝐵} ∈ ran 𝐸) |
9 | 4, 8 | anim12i 588 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
10 | 9 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
11 | | nb3graprlem1 25980 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) |
12 | | 3ancoma 1038 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
13 | 12 | biimpi 205 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
14 | | tpcoma 4229 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
15 | 14 | eqeq2i 2622 |
. . . . . . . 8
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐴, 𝐶}) |
16 | 15 | biimpi 205 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐴, 𝐶}) |
17 | 16 | anim1i 590 |
. . . . . 6
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝑉 USGrph 𝐸)) |
18 | | nb3graprlem1 25980 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
19 | 13, 17, 18 | syl2an 493 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
20 | 11, 19 | anbi12d 743 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶}) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
21 | | 3anrot 1036 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
22 | 21 | biimpri 217 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
23 | | tprot 4228 |
. . . . . . . . 9
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
24 | 23 | eqcomi 2619 |
. . . . . . . 8
⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} |
25 | 24 | eqeq2i 2622 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵}) |
26 | 25 | anbi1i 727 |
. . . . . 6
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ↔ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) |
27 | 26 | biimpi 205 |
. . . . 5
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) |
28 | | nb3graprlem1 25980 |
. . . . 5
⊢ (((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
29 | 22, 27, 28 | syl2an 493 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
30 | 10, 20, 29 | 3imtr4d 282 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶}) → (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵})) |
31 | 30 | pm4.71d 664 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶}) ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶}) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}))) |
32 | | df-3an 1033 |
. 2
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}) ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶}) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵})) |
33 | 31, 32 | syl6bbr 277 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶}) ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}))) |