Proof of Theorem nb3graprlem2
Step | Hyp | Ref
| Expression |
1 | | sneq 4135 |
. . . . . 6
⊢ (𝑣 = 𝐴 → {𝑣} = {𝐴}) |
2 | 1 | difeq2d 3690 |
. . . . 5
⊢ (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴})) |
3 | | preq1 4212 |
. . . . . 6
⊢ (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤}) |
4 | 3 | eqeq2d 2620 |
. . . . 5
⊢ (𝑣 = 𝐴 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤})) |
5 | 2, 4 | rexeqbidv 3130 |
. . . 4
⊢ (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤})) |
6 | | sneq 4135 |
. . . . . 6
⊢ (𝑣 = 𝐵 → {𝑣} = {𝐵}) |
7 | 6 | difeq2d 3690 |
. . . . 5
⊢ (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵})) |
8 | | preq1 4212 |
. . . . . 6
⊢ (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤}) |
9 | 8 | eqeq2d 2620 |
. . . . 5
⊢ (𝑣 = 𝐵 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤})) |
10 | 7, 9 | rexeqbidv 3130 |
. . . 4
⊢ (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤})) |
11 | | sneq 4135 |
. . . . . 6
⊢ (𝑣 = 𝐶 → {𝑣} = {𝐶}) |
12 | 11 | difeq2d 3690 |
. . . . 5
⊢ (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶})) |
13 | | preq1 4212 |
. . . . . 6
⊢ (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤}) |
14 | 13 | eqeq2d 2620 |
. . . . 5
⊢ (𝑣 = 𝐶 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤})) |
15 | 12, 14 | rexeqbidv 3130 |
. . . 4
⊢ (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤})) |
16 | 5, 10, 15 | rextpg 4184 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}))) |
17 | 16 | 3ad2ant1 1075 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}))) |
18 | | simpl 472 |
. . . 4
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝑉 = {𝐴, 𝐵, 𝐶}) |
19 | | difeq1 3683 |
. . . . . 6
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣})) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣})) |
21 | 20 | rexeqdv 3122 |
. . . 4
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤})) |
22 | 18, 21 | rexeqbidv 3130 |
. . 3
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤})) |
23 | 22 | 3ad2ant2 1076 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤})) |
24 | | preq2 4213 |
. . . . . . . 8
⊢ (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵}) |
25 | 24 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵})) |
26 | | preq2 4213 |
. . . . . . . 8
⊢ (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶}) |
27 | 26 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑤 = 𝐶 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶})) |
28 | 25, 27 | rexprg 4182 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}))) |
29 | 28 | 3adant1 1072 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}))) |
30 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶}) |
31 | 30 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑤 = 𝐶 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶})) |
32 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴}) |
33 | 32 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴})) |
34 | 31, 33 | rexprg 4182 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}))) |
35 | 34 | ancoms 468 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}))) |
36 | 35 | 3adant2 1073 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}))) |
37 | | preq2 4213 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴}) |
38 | 37 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴})) |
39 | | preq2 4213 |
. . . . . . . 8
⊢ (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵}) |
40 | 39 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})) |
41 | 38, 40 | rexprg 4182 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}))) |
42 | 41 | 3adant3 1074 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}))) |
43 | 29, 36, 42 | 3orbi123d 1390 |
. . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})))) |
44 | 43 | 3ad2ant1 1075 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})))) |
45 | | tprot 4228 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}) |
47 | 46 | difeq1d 3689 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴})) |
48 | | necom 2835 |
. . . . . . . . 9
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
49 | | necom 2835 |
. . . . . . . . 9
⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴) |
50 | | diftpsn3 4273 |
. . . . . . . . 9
⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶}) |
51 | 48, 49, 50 | syl2anb 495 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶}) |
52 | 51 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶}) |
53 | 47, 52 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶}) |
54 | 53 | rexeqdv 3122 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤})) |
55 | | tprot 4228 |
. . . . . . . . . 10
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
56 | 55 | eqcomi 2619 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} |
57 | 56 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}) |
58 | 57 | difeq1d 3689 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵})) |
59 | | necom 2835 |
. . . . . . . . . . . 12
⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵) |
60 | 59 | anbi1i 727 |
. . . . . . . . . . 11
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
61 | 60 | biimpi 205 |
. . . . . . . . . 10
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
62 | 61 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
63 | | diftpsn3 4273 |
. . . . . . . . 9
⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴}) |
64 | 62, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴}) |
65 | 64 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴}) |
66 | 58, 65 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴}) |
67 | 66 | rexeqdv 3122 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤})) |
68 | | diftpsn3 4273 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |
69 | 68 | 3adant1 1072 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |
70 | 69 | rexeqdv 3122 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤})) |
71 | 54, 67, 70 | 3orbi123d 1390 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}))) |
72 | 71 | 3ad2ant3 1077 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}))) |
73 | | prcom 4211 |
. . . . . . . 8
⊢ {𝐶, 𝐵} = {𝐵, 𝐶} |
74 | 73 | eqeq2i 2622 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵} ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) |
75 | 74 | orbi2i 540 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}) ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶})) |
76 | | oridm 535 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) |
77 | 75, 76 | bitr2i 264 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})) |
78 | 77 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}))) |
79 | | nbgranself2 25965 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → 𝐴 ∉ (〈𝑉, 𝐸〉 Neighbors 𝐴)) |
80 | | df-nel 2783 |
. . . . . . . . . . 11
⊢ (𝐴 ∉ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ ¬ 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴)) |
81 | | prid2g 4240 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐵, 𝐴}) |
82 | 81 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐵, 𝐴}) |
83 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴})) |
84 | 82, 83 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
85 | 84 | con3rr3 150 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴})) |
86 | 80, 85 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐴 ∉ (〈𝑉, 𝐸〉 Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴})) |
87 | 79, 86 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴})) |
88 | 87 | adantl 481 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴})) |
89 | 88 | impcom 445 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) |
90 | 89 | 3adant3 1074 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) |
91 | | biorf 419 |
. . . . . . 7
⊢ (¬
(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴} → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}))) |
92 | | orcom 401 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴})) |
93 | 91, 92 | syl6bb 275 |
. . . . . 6
⊢ (¬
(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴} → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}))) |
94 | 90, 93 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}))) |
95 | | prid2g 4240 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐶, 𝐴}) |
96 | 95 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐶, 𝐴}) |
97 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴})) |
98 | 96, 97 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
99 | 98 | con3rr3 150 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴})) |
100 | 80, 99 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐴 ∉ (〈𝑉, 𝐸〉 Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴})) |
101 | 79, 100 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴})) |
102 | 101 | adantl 481 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴})) |
103 | 102 | impcom 445 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴}) |
104 | 103 | 3adant3 1074 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴}) |
105 | | biorf 419 |
. . . . . 6
⊢ (¬
(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}))) |
106 | 104, 105 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵} ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}))) |
107 | 94, 106 | orbi12d 742 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵}) ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})))) |
108 | | prid1g 4239 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐵}) |
109 | 108 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐵}) |
110 | | eleq2 2677 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵})) |
111 | 109, 110 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
112 | 111 | con3dimp 456 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴)) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵}) |
113 | | prid1g 4239 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴, 𝐶}) |
114 | 113 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐴 ∈ {𝐴, 𝐶}) |
115 | | eleq2 2677 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶})) |
116 | 114, 115 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
117 | 116 | con3dimp 456 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴)) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}) |
118 | 112, 117 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ¬ 𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴)) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶})) |
119 | 118 | expcom 450 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}))) |
120 | 80, 119 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐴 ∉ (〈𝑉, 𝐸〉 Neighbors 𝐴) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}))) |
121 | 79, 120 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}))) |
122 | 121 | adantl 481 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}))) |
123 | 122 | impcom 445 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶})) |
124 | 123 | 3adant3 1074 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶})) |
125 | | ioran 510 |
. . . . . 6
⊢ (¬
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}) ↔ (¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶})) |
126 | 124, 125 | sylibr 223 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ¬ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶})) |
127 | 126 | 3bior1fd 1430 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})) ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})))) |
128 | 78, 107, 127 | 3bitrd 293 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ (((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐵} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐴} ∨ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝐵})))) |
129 | 44, 72, 128 | 3bitr4rd 300 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐶, 𝑤}))) |
130 | 17, 23, 129 | 3bitr4rd 300 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣, 𝑤})) |