Proof of Theorem nb3grpr2
Step | Hyp | Ref
| Expression |
1 | | 3anan32 1096 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸)) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸))) |
3 | | prcom 4668 |
. . . . . . . . . 10
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
4 | 3 | eleq1i 2829 |
. . . . . . . . 9
⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸) |
5 | 4 | biimpi 215 |
. . . . . . . 8
⊢ ({𝐶, 𝐴} ∈ 𝐸 → {𝐴, 𝐶} ∈ 𝐸) |
6 | 5 | pm4.71i 560 |
. . . . . . 7
⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)) |
7 | 6 | bianass 639 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸)) |
8 | 7 | anbi1i 624 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸)) |
9 | | anass 469 |
. . . . 5
⊢
(((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
10 | 8, 9 | bitri 274 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
11 | 2, 10 | bitrdi 287 |
. . 3
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))) |
12 | | prcom 4668 |
. . . . . . . . . 10
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} |
13 | 12 | eleq1i 2829 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸) |
14 | 13 | biimpi 215 |
. . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ 𝐸 → {𝐵, 𝐴} ∈ 𝐸) |
15 | 14 | pm4.71i 560 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)) |
16 | 15 | anbi1i 624 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐴} ∈ 𝐸)) |
17 | | df-3an 1088 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐴} ∈ 𝐸)) |
18 | 16, 17 | bitr4i 277 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) |
19 | | prcom 4668 |
. . . . . . . . . 10
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
20 | 19 | eleq1i 2829 |
. . . . . . . . 9
⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐵} ∈ 𝐸) |
21 | 20 | biimpi 215 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ 𝐸 → {𝐶, 𝐵} ∈ 𝐸) |
22 | 21 | pm4.71i 560 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)) |
23 | 22 | anbi2i 623 |
. . . . . 6
⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
24 | | 3anass 1094 |
. . . . . 6
⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
25 | 23, 24 | bitr4i 277 |
. . . . 5
⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)) |
26 | 18, 25 | anbi12i 627 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
27 | | an6 1444 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
28 | 26, 27 | bitri 274 |
. . 3
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
29 | 11, 28 | bitrdi 287 |
. 2
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))) |
30 | | nb3grpr.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
31 | | nb3grpr.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
32 | | nb3grpr.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ USGraph) |
33 | | nb3grpr.t |
. . . 4
⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) |
34 | | nb3grpr.s |
. . . 4
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
35 | 30, 31, 32, 33, 34 | nb3grprlem1 27747 |
. . 3
⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) |
36 | | tpcoma 4686 |
. . . . 5
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
37 | 33, 36 | eqtrdi 2794 |
. . . 4
⊢ (𝜑 → 𝑉 = {𝐵, 𝐴, 𝐶}) |
38 | | 3ancoma 1097 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
39 | 34, 38 | sylib 217 |
. . . 4
⊢ (𝜑 → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
40 | 30, 31, 32, 37, 39 | nb3grprlem1 27747 |
. . 3
⊢ (𝜑 → ((𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
41 | | tprot 4685 |
. . . . 5
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
42 | 33, 41 | eqtr4di 2796 |
. . . 4
⊢ (𝜑 → 𝑉 = {𝐶, 𝐴, 𝐵}) |
43 | | 3anrot 1099 |
. . . . 5
⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
44 | 34, 43 | sylibr 233 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
45 | 30, 31, 32, 42, 44 | nb3grprlem1 27747 |
. . 3
⊢ (𝜑 → ((𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
46 | 35, 40, 45 | 3anbi123d 1435 |
. 2
⊢ (𝜑 → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵}) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))) |
47 | 29, 46 | bitr4d 281 |
1
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵}))) |