Proof of Theorem nb3grpr2
Step | Hyp | Ref
| Expression |
1 | | 3anan32 1050 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸)) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸))) |
3 | | prcom 4267 |
. . . . . . . . . . 11
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
4 | 3 | eleq1i 2692 |
. . . . . . . . . 10
⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸) |
5 | 4 | biimpi 206 |
. . . . . . . . 9
⊢ ({𝐶, 𝐴} ∈ 𝐸 → {𝐴, 𝐶} ∈ 𝐸) |
6 | 5 | pm4.71i 664 |
. . . . . . . 8
⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)) |
7 | 6 | anbi2i 730 |
. . . . . . 7
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) |
8 | | anass 681 |
. . . . . . 7
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) |
9 | 7, 8 | bitr4i 267 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸)) |
10 | 9 | anbi1i 731 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸)) |
11 | | anass 681 |
. . . . 5
⊢
(((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
12 | 10, 11 | bitri 264 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
13 | 2, 12 | syl6bb 276 |
. . 3
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))) |
14 | | prcom 4267 |
. . . . . . . . . 10
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} |
15 | 14 | eleq1i 2692 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸) |
16 | 15 | biimpi 206 |
. . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ 𝐸 → {𝐵, 𝐴} ∈ 𝐸) |
17 | 16 | pm4.71i 664 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)) |
18 | 17 | anbi1i 731 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐴} ∈ 𝐸)) |
19 | | df-3an 1039 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐴} ∈ 𝐸)) |
20 | 18, 19 | bitr4i 267 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) |
21 | | prcom 4267 |
. . . . . . . . . 10
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
22 | 21 | eleq1i 2692 |
. . . . . . . . 9
⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐵} ∈ 𝐸) |
23 | 22 | biimpi 206 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ 𝐸 → {𝐶, 𝐵} ∈ 𝐸) |
24 | 23 | pm4.71i 664 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)) |
25 | 24 | anbi2i 730 |
. . . . . 6
⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
26 | | 3anass 1042 |
. . . . . 6
⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
27 | 25, 26 | bitr4i 267 |
. . . . 5
⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)) |
28 | 20, 27 | anbi12i 733 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
29 | | an6 1408 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
30 | 28, 29 | bitri 264 |
. . 3
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
31 | 13, 30 | syl6bb 276 |
. 2
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))) |
32 | | nb3grpr.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
33 | | nb3grpr.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
34 | | nb3grpr.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ USGraph ) |
35 | | nb3grpr.t |
. . . 4
⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) |
36 | | nb3grpr.s |
. . . 4
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
37 | 32, 33, 34, 35, 36 | nb3grprlem1 26282 |
. . 3
⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) |
38 | | tpcoma 4285 |
. . . . 5
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
39 | 35, 38 | syl6eq 2672 |
. . . 4
⊢ (𝜑 → 𝑉 = {𝐵, 𝐴, 𝐶}) |
40 | | 3ancoma 1045 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
41 | 36, 40 | sylib 208 |
. . . 4
⊢ (𝜑 → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
42 | 32, 33, 34, 39, 41 | nb3grprlem1 26282 |
. . 3
⊢ (𝜑 → ((𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
43 | | tprot 4284 |
. . . . 5
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
44 | 35, 43 | syl6eqr 2674 |
. . . 4
⊢ (𝜑 → 𝑉 = {𝐶, 𝐴, 𝐵}) |
45 | | 3anrot 1043 |
. . . . 5
⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
46 | 36, 45 | sylibr 224 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
47 | 32, 33, 34, 44, 46 | nb3grprlem1 26282 |
. . 3
⊢ (𝜑 → ((𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))) |
48 | 37, 42, 47 | 3anbi123d 1399 |
. 2
⊢ (𝜑 → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵}) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))) |
49 | 31, 48 | bitr4d 271 |
1
⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵}))) |