Metamath Proof Explorer

Theorem 3vfriswmgr

Description: Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ⊢ V = Vtx ⁡ G
3vfriswmgr.e ⊢ E = Edg ⁡ G
Assertion 3vfriswmgr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ V = Vtx ⁡ G
2 3vfriswmgr.e ⊢ E = Edg ⁡ G
3 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
4 1 2 frgr3v ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → V = A B C ∧ G ∈ USGraph → G ∈ FriendGraph ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
5 4 exp4b ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → A ≠ B ∧ A ≠ C ∧ B ≠ C → V = A B C → G ∈ USGraph → G ∈ FriendGraph ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
6 5 3imp1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → G ∈ FriendGraph ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
7 prcom ⊢ C A = A C
8 7 eleq1i ⊢ C A ∈ E ↔ A C ∈ E
9 8 biimpi ⊢ C A ∈ E → A C ∈ E
10 9 3ad2ant3 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A C ∈ E
11 10 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A C ∈ E
12 simpl11 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ∈ X
13 simpl12 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ∈ Y
14 simp1 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A ≠ B
15 14 3ad2ant2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → A ≠ B
16 15 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ≠ B
17 12 13 16 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ A ≠ B
18 simp3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → V = A B C
19 18 anim1i ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → V = A B C ∧ G ∈ USGraph
20 17 19 jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph
21 simp1 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A B ∈ E
22 1 2 3vfriswmgrlem ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph → A B ∈ E → ∃! w ∈ A B A w ∈ E
23 22 imp ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∃! w ∈ A B A w ∈ E
24 20 21 23 syl2an ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃! w ∈ A B A w ∈ E
25 11 24 jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A C ∈ E ∧ ∃! w ∈ A B A w ∈ E
26 simpr2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → B C ∈ E
27 necom ⊢ A ≠ B ↔ B ≠ A
28 27 biimpi ⊢ A ≠ B → B ≠ A
29 28 3ad2ant1 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → B ≠ A
30 29 3ad2ant2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → B ≠ A
31 30 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ≠ A
32 13 12 31 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ∈ Y ∧ A ∈ X ∧ B ≠ A
33 tpcoma ⊢ A B C = B A C
34 18 33 eqtrdi ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → V = B A C
35 34 anim1i ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → V = B A C ∧ G ∈ USGraph
36 32 35 jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ∈ Y ∧ A ∈ X ∧ B ≠ A ∧ V = B A C ∧ G ∈ USGraph
37 prcom ⊢ A B = B A
38 37 eleq1i ⊢ A B ∈ E ↔ B A ∈ E
39 38 biimpi ⊢ A B ∈ E → B A ∈ E
40 39 3ad2ant1 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → B A ∈ E
41 1 2 3vfriswmgrlem ⊢ B ∈ Y ∧ A ∈ X ∧ B ≠ A ∧ V = B A C ∧ G ∈ USGraph → B A ∈ E → ∃! w ∈ B A B w ∈ E
42 41 imp ⊢ B ∈ Y ∧ A ∈ X ∧ B ≠ A ∧ V = B A C ∧ G ∈ USGraph ∧ B A ∈ E → ∃! w ∈ B A B w ∈ E
43 reueq1 ⊢ A B = B A → ∃! w ∈ A B B w ∈ E ↔ ∃! w ∈ B A B w ∈ E
44 37 43 ax-mp ⊢ ∃! w ∈ A B B w ∈ E ↔ ∃! w ∈ B A B w ∈ E
45 42 44 sylibr ⊢ B ∈ Y ∧ A ∈ X ∧ B ≠ A ∧ V = B A C ∧ G ∈ USGraph ∧ B A ∈ E → ∃! w ∈ A B B w ∈ E
46 36 40 45 syl2an ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃! w ∈ A B B w ∈ E
47 26 46 jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
48 25 47 jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A C ∈ E ∧ ∃! w ∈ A B A w ∈ E ∧ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
49 preq1 ⊢ v = A → v C = A C
50 49 eleq1d ⊢ v = A → v C ∈ E ↔ A C ∈ E
51 preq1 ⊢ v = A → v w = A w
52 51 eleq1d ⊢ v = A → v w ∈ E ↔ A w ∈ E
53 52 reubidv ⊢ v = A → ∃! w ∈ A B v w ∈ E ↔ ∃! w ∈ A B A w ∈ E
54 50 53 anbi12d ⊢ v = A → v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ A C ∈ E ∧ ∃! w ∈ A B A w ∈ E
55 preq1 ⊢ v = B → v C = B C
56 55 eleq1d ⊢ v = B → v C ∈ E ↔ B C ∈ E
57 preq1 ⊢ v = B → v w = B w
58 57 eleq1d ⊢ v = B → v w ∈ E ↔ B w ∈ E
59 58 reubidv ⊢ v = B → ∃! w ∈ A B v w ∈ E ↔ ∃! w ∈ A B B w ∈ E
60 56 59 anbi12d ⊢ v = B → v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
61 54 60 ralprg ⊢ A ∈ X ∧ B ∈ Y → ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ A C ∈ E ∧ ∃! w ∈ A B A w ∈ E ∧ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
62 61 3adant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ A C ∈ E ∧ ∃! w ∈ A B A w ∈ E ∧ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
63 62 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ A C ∈ E ∧ ∃! w ∈ A B A w ∈ E ∧ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
64 63 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ A C ∈ E ∧ ∃! w ∈ A B A w ∈ E ∧ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
65 64 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E ↔ A C ∈ E ∧ ∃! w ∈ A B A w ∈ E ∧ B C ∈ E ∧ ∃! w ∈ A B B w ∈ E
66 48 65 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E
67 diftpsn3 ⊢ A ≠ C ∧ B ≠ C → A B C ∖ C = A B
68 67 3adant1 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ C = A B
69 reueq1 ⊢ A B C ∖ C = A B → ∃! w ∈ A B C ∖ C v w ∈ E ↔ ∃! w ∈ A B v w ∈ E
70 68 69 syl ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃! w ∈ A B C ∖ C v w ∈ E ↔ ∃! w ∈ A B v w ∈ E
71 70 anbi2d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E ↔ v C ∈ E ∧ ∃! w ∈ A B v w ∈ E
72 68 71 raleqbidv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E ↔ ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E
73 72 3ad2ant2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E ↔ ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E
74 73 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E ↔ ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E
75 74 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E ↔ ∀ v ∈ A B v C ∈ E ∧ ∃! w ∈ A B v w ∈ E
76 66 75 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
77 76 3mix3d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∀ v ∈ A B C ∖ A v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E ∨ ∀ v ∈ A B C ∖ B v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E ∨ ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
78 sneq ⊢ h = A → h = A
79 78 difeq2d ⊢ h = A → A B C ∖ h = A B C ∖ A
80 preq2 ⊢ h = A → v h = v A
81 80 eleq1d ⊢ h = A → v h ∈ E ↔ v A ∈ E
82 reueq1 ⊢ A B C ∖ h = A B C ∖ A → ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ A v w ∈ E
83 79 82 syl ⊢ h = A → ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ A v w ∈ E
84 81 83 anbi12d ⊢ h = A → v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E
85 79 84 raleqbidv ⊢ h = A → ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ A v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E
86 sneq ⊢ h = B → h = B
87 86 difeq2d ⊢ h = B → A B C ∖ h = A B C ∖ B
88 preq2 ⊢ h = B → v h = v B
89 88 eleq1d ⊢ h = B → v h ∈ E ↔ v B ∈ E
90 reueq1 ⊢ A B C ∖ h = A B C ∖ B → ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ B v w ∈ E
91 87 90 syl ⊢ h = B → ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ B v w ∈ E
92 89 91 anbi12d ⊢ h = B → v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E
93 87 92 raleqbidv ⊢ h = B → ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ B v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E
94 sneq ⊢ h = C → h = C
95 94 difeq2d ⊢ h = C → A B C ∖ h = A B C ∖ C
96 preq2 ⊢ h = C → v h = v C
97 96 eleq1d ⊢ h = C → v h ∈ E ↔ v C ∈ E
98 reueq1 ⊢ A B C ∖ h = A B C ∖ C → ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ C v w ∈ E
99 95 98 syl ⊢ h = C → ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ C v w ∈ E
100 97 99 anbi12d ⊢ h = C → v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
101 95 100 raleqbidv ⊢ h = C → ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
102 85 93 101 rextpg ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ A v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E ∨ ∀ v ∈ A B C ∖ B v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E ∨ ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
103 102 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ A v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E ∨ ∀ v ∈ A B C ∖ B v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E ∨ ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
104 103 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ A v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E ∨ ∀ v ∈ A B C ∖ B v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E ∨ ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
105 104 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ A v A ∈ E ∧ ∃! w ∈ A B C ∖ A v w ∈ E ∨ ∀ v ∈ A B C ∖ B v B ∈ E ∧ ∃! w ∈ A B C ∖ B v w ∈ E ∨ ∀ v ∈ A B C ∖ C v C ∈ E ∧ ∃! w ∈ A B C ∖ C v w ∈ E
106 77 105 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
107 106 ex ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
108 6 107 sylbid ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → G ∈ FriendGraph → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
109 108 expcom ⊢ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → G ∈ FriendGraph → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
110 109 com23 ⊢ G ∈ USGraph → G ∈ FriendGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
111 3 110 mpcom ⊢ G ∈ FriendGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
112 111 com12 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → G ∈ FriendGraph → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
113 difeq1 ⊢ V = A B C → V ∖ h = A B C ∖ h
114 reueq1 ⊢ V ∖ h = A B C ∖ h → ∃! w ∈ V ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ h v w ∈ E
115 113 114 syl ⊢ V = A B C → ∃! w ∈ V ∖ h v w ∈ E ↔ ∃! w ∈ A B C ∖ h v w ∈ E
116 115 anbi2d ⊢ V = A B C → v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E ↔ v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
117 113 116 raleqbidv ⊢ V = A B C → ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E ↔ ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
118 117 rexeqbi1dv ⊢ V = A B C → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E ↔ ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
119 118 imbi2d ⊢ V = A B C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E ↔ G ∈ FriendGraph → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
120 119 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E ↔ G ∈ FriendGraph → ∃ h ∈ A B C ∀ v ∈ A B C ∖ h v h ∈ E ∧ ∃! w ∈ A B C ∖ h v w ∈ E
121 112 120 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C → G ∈ FriendGraph → ∃ h ∈ V ∀ v ∈ V ∖ h v h ∈ E ∧ ∃! w ∈ V ∖ h v w ∈ E