Metamath Proof Explorer

Theorem frgr3v

Description: Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frgr3v.v ⊢ V = Vtx ⁡ G
frgr3v.e ⊢ E = Edg ⁡ G
Assertion 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

Proof

Step Hyp Ref Expression
1 frgr3v.v ⊢ V = Vtx ⁡ G
2 frgr3v.e ⊢ E = Edg ⁡ G
3 1 2 isfrgr ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E
4 3 a1i ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E
5 id ⊢ V = A B C → V = A B C
6 difeq1 ⊢ V = A B C → V ∖ k = A B C ∖ k
7 reueq1 ⊢ V = A B C → ∃! x ∈ V x k x l ⊆ E ↔ ∃! x ∈ A B C x k x l ⊆ E
8 6 7 raleqbidv ⊢ V = A B C → ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E ↔ ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E
9 5 8 raleqbidv ⊢ V = A B C → ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E ↔ ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E
10 9 anbi2d ⊢ V = A B C → G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E ↔ G ∈ USGraph ∧ ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E
11 10 baibd ⊢ V = A B C ∧ G ∈ USGraph → G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E ↔ ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E
12 11 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E ↔ ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E
13 4 12 bitrd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → G ∈ FriendGraph ↔ ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E
14 sneq ⊢ k = A → k = A
15 14 difeq2d ⊢ k = A → A B C ∖ k = A B C ∖ A
16 preq2 ⊢ k = A → x k = x A
17 16 preq1d ⊢ k = A → x k x l = x A x l
18 17 sseq1d ⊢ k = A → x k x l ⊆ E ↔ x A x l ⊆ E
19 18 reubidv ⊢ k = A → ∃! x ∈ A B C x k x l ⊆ E ↔ ∃! x ∈ A B C x A x l ⊆ E
20 15 19 raleqbidv ⊢ k = A → ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E ↔ ∀ l ∈ A B C ∖ A ∃! x ∈ A B C x A x l ⊆ E
21 sneq ⊢ k = B → k = B
22 21 difeq2d ⊢ k = B → A B C ∖ k = A B C ∖ B
23 preq2 ⊢ k = B → x k = x B
24 23 preq1d ⊢ k = B → x k x l = x B x l
25 24 sseq1d ⊢ k = B → x k x l ⊆ E ↔ x B x l ⊆ E
26 25 reubidv ⊢ k = B → ∃! x ∈ A B C x k x l ⊆ E ↔ ∃! x ∈ A B C x B x l ⊆ E
27 22 26 raleqbidv ⊢ k = B → ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E ↔ ∀ l ∈ A B C ∖ B ∃! x ∈ A B C x B x l ⊆ E
28 sneq ⊢ k = C → k = C
29 28 difeq2d ⊢ k = C → A B C ∖ k = A B C ∖ C
30 preq2 ⊢ k = C → x k = x C
31 30 preq1d ⊢ k = C → x k x l = x C x l
32 31 sseq1d ⊢ k = C → x k x l ⊆ E ↔ x C x l ⊆ E
33 32 reubidv ⊢ k = C → ∃! x ∈ A B C x k x l ⊆ E ↔ ∃! x ∈ A B C x C x l ⊆ E
34 29 33 raleqbidv ⊢ k = C → ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E ↔ ∀ l ∈ A B C ∖ C ∃! x ∈ A B C x C x l ⊆ E
35 20 27 34 raltpg ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E ↔ ∀ l ∈ A B C ∖ A ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ A B C ∖ B ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B C ∖ C ∃! x ∈ A B C x C x l ⊆ E
36 35 ad2antrr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E ↔ ∀ l ∈ A B C ∖ A ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ A B C ∖ B ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B C ∖ C ∃! x ∈ A B C x C x l ⊆ E
37 tprot ⊢ A B C = B C A
38 37 a1i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C = B C A
39 38 difeq1d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ A = B C A ∖ A
40 necom ⊢ A ≠ B ↔ B ≠ A
41 40 biimpi ⊢ A ≠ B → B ≠ A
42 necom ⊢ A ≠ C ↔ C ≠ A
43 42 biimpi ⊢ A ≠ C → C ≠ A
44 41 43 anim12i ⊢ A ≠ B ∧ A ≠ C → B ≠ A ∧ C ≠ A
45 44 3adant3 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → B ≠ A ∧ C ≠ A
46 diftpsn3 ⊢ B ≠ A ∧ C ≠ A → B C A ∖ A = B C
47 45 46 syl ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → B C A ∖ A = B C
48 39 47 eqtrd ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ A = B C
49 48 raleqdv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∀ l ∈ A B C ∖ A ∃! x ∈ A B C x A x l ⊆ E ↔ ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E
50 tprot ⊢ C A B = A B C
51 50 eqcomi ⊢ A B C = C A B
52 51 a1i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C = C A B
53 52 difeq1d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ B = C A B ∖ B
54 id ⊢ A ≠ B → A ≠ B
55 necom ⊢ B ≠ C ↔ C ≠ B
56 55 biimpi ⊢ B ≠ C → C ≠ B
57 54 56 anim12ci ⊢ A ≠ B ∧ B ≠ C → C ≠ B ∧ A ≠ B
58 57 3adant2 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → C ≠ B ∧ A ≠ B
59 diftpsn3 ⊢ C ≠ B ∧ A ≠ B → C A B ∖ B = C A
60 58 59 syl ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → C A B ∖ B = C A
61 53 60 eqtrd ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ B = C A
62 61 raleqdv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∀ l ∈ A B C ∖ B ∃! x ∈ A B C x B x l ⊆ E ↔ ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E
63 diftpsn3 ⊢ A ≠ C ∧ B ≠ C → A B C ∖ C = A B
64 63 3adant1 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ C = A B
65 64 raleqdv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∀ l ∈ A B C ∖ C ∃! x ∈ A B C x C x l ⊆ E ↔ ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E
66 49 62 65 3anbi123d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∀ l ∈ A B C ∖ A ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ A B C ∖ B ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B C ∖ C ∃! x ∈ A B C x C x l ⊆ E ↔ ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E
67 66 ad2antlr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ l ∈ A B C ∖ A ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ A B C ∖ B ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B C ∖ C ∃! x ∈ A B C x C x l ⊆ E ↔ ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E
68 preq2 ⊢ l = B → x l = x B
69 68 preq2d ⊢ l = B → x A x l = x A x B
70 69 sseq1d ⊢ l = B → x A x l ⊆ E ↔ x A x B ⊆ E
71 70 reubidv ⊢ l = B → ∃! x ∈ A B C x A x l ⊆ E ↔ ∃! x ∈ A B C x A x B ⊆ E
72 preq2 ⊢ l = C → x l = x C
73 72 preq2d ⊢ l = C → x A x l = x A x C
74 73 sseq1d ⊢ l = C → x A x l ⊆ E ↔ x A x C ⊆ E
75 74 reubidv ⊢ l = C → ∃! x ∈ A B C x A x l ⊆ E ↔ ∃! x ∈ A B C x A x C ⊆ E
76 71 75 ralprg ⊢ B ∈ Y ∧ C ∈ Z → ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E ↔ ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E
77 76 3adant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E ↔ ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E
78 72 preq2d ⊢ l = C → x B x l = x B x C
79 78 sseq1d ⊢ l = C → x B x l ⊆ E ↔ x B x C ⊆ E
80 79 reubidv ⊢ l = C → ∃! x ∈ A B C x B x l ⊆ E ↔ ∃! x ∈ A B C x B x C ⊆ E
81 preq2 ⊢ l = A → x l = x A
82 81 preq2d ⊢ l = A → x B x l = x B x A
83 82 sseq1d ⊢ l = A → x B x l ⊆ E ↔ x B x A ⊆ E
84 83 reubidv ⊢ l = A → ∃! x ∈ A B C x B x l ⊆ E ↔ ∃! x ∈ A B C x B x A ⊆ E
85 80 84 ralprg ⊢ C ∈ Z ∧ A ∈ X → ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ↔ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E
86 85 ancoms ⊢ A ∈ X ∧ C ∈ Z → ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ↔ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E
87 86 3adant2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ↔ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E
88 81 preq2d ⊢ l = A → x C x l = x C x A
89 88 sseq1d ⊢ l = A → x C x l ⊆ E ↔ x C x A ⊆ E
90 89 reubidv ⊢ l = A → ∃! x ∈ A B C x C x l ⊆ E ↔ ∃! x ∈ A B C x C x A ⊆ E
91 68 preq2d ⊢ l = B → x C x l = x C x B
92 91 sseq1d ⊢ l = B → x C x l ⊆ E ↔ x C x B ⊆ E
93 92 reubidv ⊢ l = B → ∃! x ∈ A B C x C x l ⊆ E ↔ ∃! x ∈ A B C x C x B ⊆ E
94 90 93 ralprg ⊢ A ∈ X ∧ B ∈ Y → ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E ↔ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E
95 94 3adant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E ↔ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E
96 77 87 95 3anbi123d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E ↔ ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E ∧ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E ∧ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E
97 96 ad2antrr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ l ∈ B C ∃! x ∈ A B C x A x l ⊆ E ∧ ∀ l ∈ C A ∃! x ∈ A B C x B x l ⊆ E ∧ ∀ l ∈ A B ∃! x ∈ A B C x C x l ⊆ E ↔ ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E ∧ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E ∧ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E
98 36 67 97 3bitrd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ k ∈ A B C ∀ l ∈ A B C ∖ k ∃! x ∈ A B C x k x l ⊆ E ↔ ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E ∧ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E ∧ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E
99 1 2 frgr3vlem2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x A x B ⊆ E ↔ C A ∈ E ∧ C B ∈ E
100 99 imp ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x A x B ⊆ E ↔ C A ∈ E ∧ C B ∈ E
101 simpll1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ∈ X
102 simpll3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C ∈ Z
103 simpll2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ∈ Y
104 101 102 103 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ∈ X ∧ C ∈ Z ∧ B ∈ Y
105 simplr2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ≠ C
106 simplr1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ≠ B
107 58 simpld ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → C ≠ B
108 107 ad2antlr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C ≠ B
109 105 106 108 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A ≠ C ∧ A ≠ B ∧ C ≠ B
110 tpcomb ⊢ A B C = A C B
111 5 110 eqtrdi ⊢ V = A B C → V = A C B
112 111 anim1i ⊢ V = A B C ∧ G ∈ USGraph → V = A C B ∧ G ∈ USGraph
113 112 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → V = A C B ∧ G ∈ USGraph
114 reueq1 ⊢ A B C = A C B → ∃! x ∈ A B C x A x C ⊆ E ↔ ∃! x ∈ A C B x A x C ⊆ E
115 110 114 mp1i ⊢ A ∈ X ∧ C ∈ Z ∧ B ∈ Y ∧ A ≠ C ∧ A ≠ B ∧ C ≠ B ∧ V = A C B ∧ G ∈ USGraph → ∃! x ∈ A B C x A x C ⊆ E ↔ ∃! x ∈ A C B x A x C ⊆ E
116 1 2 frgr3vlem2 ⊢ A ∈ X ∧ C ∈ Z ∧ B ∈ Y ∧ A ≠ C ∧ A ≠ B ∧ C ≠ B → V = A C B ∧ G ∈ USGraph → ∃! x ∈ A C B x A x C ⊆ E ↔ B A ∈ E ∧ B C ∈ E
117 116 imp ⊢ A ∈ X ∧ C ∈ Z ∧ B ∈ Y ∧ A ≠ C ∧ A ≠ B ∧ C ≠ B ∧ V = A C B ∧ G ∈ USGraph → ∃! x ∈ A C B x A x C ⊆ E ↔ B A ∈ E ∧ B C ∈ E
118 115 117 bitrd ⊢ A ∈ X ∧ C ∈ Z ∧ B ∈ Y ∧ A ≠ C ∧ A ≠ B ∧ C ≠ B ∧ V = A C B ∧ G ∈ USGraph → ∃! x ∈ A B C x A x C ⊆ E ↔ B A ∈ E ∧ B C ∈ E
119 104 109 113 118 syl21anc ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x A x C ⊆ E ↔ B A ∈ E ∧ B C ∈ E
120 100 119 anbi12d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E ↔ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ B C ∈ E
121 103 102 101 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ∈ Y ∧ C ∈ Z ∧ A ∈ X
122 simplr3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ≠ C
123 106 necomd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ≠ A
124 105 necomd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C ≠ A
125 122 123 124 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ≠ C ∧ B ≠ A ∧ C ≠ A
126 37 eqeq2i ⊢ V = A B C ↔ V = B C A
127 126 biimpi ⊢ V = A B C → V = B C A
128 127 anim1i ⊢ V = A B C ∧ G ∈ USGraph → V = B C A ∧ G ∈ USGraph
129 128 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → V = B C A ∧ G ∈ USGraph
130 reueq1 ⊢ A B C = B C A → ∃! x ∈ A B C x B x C ⊆ E ↔ ∃! x ∈ B C A x B x C ⊆ E
131 37 130 mp1i ⊢ B ∈ Y ∧ C ∈ Z ∧ A ∈ X ∧ B ≠ C ∧ B ≠ A ∧ C ≠ A ∧ V = B C A ∧ G ∈ USGraph → ∃! x ∈ A B C x B x C ⊆ E ↔ ∃! x ∈ B C A x B x C ⊆ E
132 1 2 frgr3vlem2 ⊢ B ∈ Y ∧ C ∈ Z ∧ A ∈ X ∧ B ≠ C ∧ B ≠ A ∧ C ≠ A → V = B C A ∧ G ∈ USGraph → ∃! x ∈ B C A x B x C ⊆ E ↔ A B ∈ E ∧ A C ∈ E
133 132 imp ⊢ B ∈ Y ∧ C ∈ Z ∧ A ∈ X ∧ B ≠ C ∧ B ≠ A ∧ C ≠ A ∧ V = B C A ∧ G ∈ USGraph → ∃! x ∈ B C A x B x C ⊆ E ↔ A B ∈ E ∧ A C ∈ E
134 131 133 bitrd ⊢ B ∈ Y ∧ C ∈ Z ∧ A ∈ X ∧ B ≠ C ∧ B ≠ A ∧ C ≠ A ∧ V = B C A ∧ G ∈ USGraph → ∃! x ∈ A B C x B x C ⊆ E ↔ A B ∈ E ∧ A C ∈ E
135 121 125 129 134 syl21anc ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x B x C ⊆ E ↔ A B ∈ E ∧ A C ∈ E
136 103 101 102 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ∈ Y ∧ A ∈ X ∧ C ∈ Z
137 123 122 105 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B ≠ A ∧ B ≠ C ∧ A ≠ C
138 tpcoma ⊢ A B C = B A C
139 138 eqeq2i ⊢ V = A B C ↔ V = B A C
140 139 biimpi ⊢ V = A B C → V = B A C
141 140 anim1i ⊢ V = A B C ∧ G ∈ USGraph → V = B A C ∧ G ∈ USGraph
142 141 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → V = B A C ∧ G ∈ USGraph
143 reueq1 ⊢ A B C = B A C → ∃! x ∈ A B C x B x A ⊆ E ↔ ∃! x ∈ B A C x B x A ⊆ E
144 138 143 mp1i ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ B ≠ A ∧ B ≠ C ∧ A ≠ C ∧ V = B A C ∧ G ∈ USGraph → ∃! x ∈ A B C x B x A ⊆ E ↔ ∃! x ∈ B A C x B x A ⊆ E
145 1 2 frgr3vlem2 ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ B ≠ A ∧ B ≠ C ∧ A ≠ C → V = B A C ∧ G ∈ USGraph → ∃! x ∈ B A C x B x A ⊆ E ↔ C B ∈ E ∧ C A ∈ E
146 145 imp ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ B ≠ A ∧ B ≠ C ∧ A ≠ C ∧ V = B A C ∧ G ∈ USGraph → ∃! x ∈ B A C x B x A ⊆ E ↔ C B ∈ E ∧ C A ∈ E
147 144 146 bitrd ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ B ≠ A ∧ B ≠ C ∧ A ≠ C ∧ V = B A C ∧ G ∈ USGraph → ∃! x ∈ A B C x B x A ⊆ E ↔ C B ∈ E ∧ C A ∈ E
148 136 137 142 147 syl21anc ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x B x A ⊆ E ↔ C B ∈ E ∧ C A ∈ E
149 135 148 anbi12d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E ↔ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ C A ∈ E
150 102 101 103 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C ∈ Z ∧ A ∈ X ∧ B ∈ Y
151 124 108 106 3jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C ≠ A ∧ C ≠ B ∧ A ≠ B
152 51 eqeq2i ⊢ V = A B C ↔ V = C A B
153 152 biimpi ⊢ V = A B C → V = C A B
154 153 anim1i ⊢ V = A B C ∧ G ∈ USGraph → V = C A B ∧ G ∈ USGraph
155 154 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → V = C A B ∧ G ∈ USGraph
156 reueq1 ⊢ A B C = C A B → ∃! x ∈ A B C x C x A ⊆ E ↔ ∃! x ∈ C A B x C x A ⊆ E
157 51 156 mp1i ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ C ≠ A ∧ C ≠ B ∧ A ≠ B ∧ V = C A B ∧ G ∈ USGraph → ∃! x ∈ A B C x C x A ⊆ E ↔ ∃! x ∈ C A B x C x A ⊆ E
158 1 2 frgr3vlem2 ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ C ≠ A ∧ C ≠ B ∧ A ≠ B → V = C A B ∧ G ∈ USGraph → ∃! x ∈ C A B x C x A ⊆ E ↔ B C ∈ E ∧ B A ∈ E
159 158 imp ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ C ≠ A ∧ C ≠ B ∧ A ≠ B ∧ V = C A B ∧ G ∈ USGraph → ∃! x ∈ C A B x C x A ⊆ E ↔ B C ∈ E ∧ B A ∈ E
160 157 159 bitrd ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ C ≠ A ∧ C ≠ B ∧ A ≠ B ∧ V = C A B ∧ G ∈ USGraph → ∃! x ∈ A B C x C x A ⊆ E ↔ B C ∈ E ∧ B A ∈ E
161 150 151 155 160 syl21anc ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x C x A ⊆ E ↔ B C ∈ E ∧ B A ∈ E
162 3anrev ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ↔ C ∈ Z ∧ B ∈ Y ∧ A ∈ X
163 162 biimpi ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C ∈ Z ∧ B ∈ Y ∧ A ∈ X
164 55 42 40 3anbi123i ⊢ B ≠ C ∧ A ≠ C ∧ A ≠ B ↔ C ≠ B ∧ C ≠ A ∧ B ≠ A
165 164 biimpi ⊢ B ≠ C ∧ A ≠ C ∧ A ≠ B → C ≠ B ∧ C ≠ A ∧ B ≠ A
166 165 3com13 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → C ≠ B ∧ C ≠ A ∧ B ≠ A
167 163 166 anim12i ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → C ∈ Z ∧ B ∈ Y ∧ A ∈ X ∧ C ≠ B ∧ C ≠ A ∧ B ≠ A
168 tpcoma ⊢ B C A = C B A
169 37 168 eqtri ⊢ A B C = C B A
170 169 eqeq2i ⊢ V = A B C ↔ V = C B A
171 170 biimpi ⊢ V = A B C → V = C B A
172 171 anim1i ⊢ V = A B C ∧ G ∈ USGraph → V = C B A ∧ G ∈ USGraph
173 reueq1 ⊢ A B C = C B A → ∃! x ∈ A B C x C x B ⊆ E ↔ ∃! x ∈ C B A x C x B ⊆ E
174 169 173 mp1i ⊢ C ∈ Z ∧ B ∈ Y ∧ A ∈ X ∧ C ≠ B ∧ C ≠ A ∧ B ≠ A ∧ V = C B A ∧ G ∈ USGraph → ∃! x ∈ A B C x C x B ⊆ E ↔ ∃! x ∈ C B A x C x B ⊆ E
175 1 2 frgr3vlem2 ⊢ C ∈ Z ∧ B ∈ Y ∧ A ∈ X ∧ C ≠ B ∧ C ≠ A ∧ B ≠ A → V = C B A ∧ G ∈ USGraph → ∃! x ∈ C B A x C x B ⊆ E ↔ A C ∈ E ∧ A B ∈ E
176 175 imp ⊢ C ∈ Z ∧ B ∈ Y ∧ A ∈ X ∧ C ≠ B ∧ C ≠ A ∧ B ≠ A ∧ V = C B A ∧ G ∈ USGraph → ∃! x ∈ C B A x C x B ⊆ E ↔ A C ∈ E ∧ A B ∈ E
177 174 176 bitrd ⊢ C ∈ Z ∧ B ∈ Y ∧ A ∈ X ∧ C ≠ B ∧ C ≠ A ∧ B ≠ A ∧ V = C B A ∧ G ∈ USGraph → ∃! x ∈ A B C x C x B ⊆ E ↔ A C ∈ E ∧ A B ∈ E
178 167 172 177 syl2an ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x C x B ⊆ E ↔ A C ∈ E ∧ A B ∈ E
179 161 178 anbi12d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E ↔ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ A B ∈ E
180 120 149 179 3anbi123d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E ∧ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E ∧ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E ↔ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ B C ∈ E ∧ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ C A ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ A B ∈ E
181 prcom ⊢ B C = C B
182 181 eleq1i ⊢ B C ∈ E ↔ C B ∈ E
183 182 anbi2i ⊢ B A ∈ E ∧ B C ∈ E ↔ B A ∈ E ∧ C B ∈ E
184 183 anbi2i ⊢ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ B C ∈ E ↔ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ C B ∈ E
185 anandir ⊢ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E ↔ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ C B ∈ E
186 184 185 bitr4i ⊢ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ B C ∈ E ↔ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E
187 prcom ⊢ C A = A C
188 187 eleq1i ⊢ C A ∈ E ↔ A C ∈ E
189 188 anbi2i ⊢ C B ∈ E ∧ C A ∈ E ↔ C B ∈ E ∧ A C ∈ E
190 189 anbi2i ⊢ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ A C ∈ E
191 anandir ⊢ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E ↔ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ A C ∈ E
192 190 191 bitr4i ⊢ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E
193 prcom ⊢ A B = B A
194 193 eleq1i ⊢ A B ∈ E ↔ B A ∈ E
195 194 anbi2i ⊢ A C ∈ E ∧ A B ∈ E ↔ A C ∈ E ∧ B A ∈ E
196 195 anbi2i ⊢ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ A B ∈ E ↔ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ B A ∈ E
197 anandir ⊢ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E ↔ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ B A ∈ E
198 196 197 bitr4i ⊢ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ A B ∈ E ↔ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E
199 186 192 198 3anbi123i ⊢ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ B C ∈ E ∧ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ C A ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ A B ∈ E ↔ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E ∧ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E ∧ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E
200 3anrot ⊢ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E ↔ B A ∈ E ∧ C B ∈ E ∧ C A ∈ E
201 df-3an ⊢ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E ↔ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E
202 prcom ⊢ B A = A B
203 202 eleq1i ⊢ B A ∈ E ↔ A B ∈ E
204 prcom ⊢ C B = B C
205 204 eleq1i ⊢ C B ∈ E ↔ B C ∈ E
206 biid ⊢ C A ∈ E ↔ C A ∈ E
207 203 205 206 3anbi123i ⊢ B A ∈ E ∧ C B ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
208 200 201 207 3bitr3i ⊢ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
209 df-3an ⊢ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E ↔ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E
210 biid ⊢ A B ∈ E ↔ A B ∈ E
211 prcom ⊢ A C = C A
212 211 eleq1i ⊢ A C ∈ E ↔ C A ∈ E
213 210 205 212 3anbi123i ⊢ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
214 209 213 bitr3i ⊢ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
215 df-3an ⊢ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E ↔ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E
216 3anrot ⊢ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E ↔ A C ∈ E ∧ B A ∈ E ∧ B C ∈ E
217 3anrot ⊢ A C ∈ E ∧ B A ∈ E ∧ B C ∈ E ↔ B A ∈ E ∧ B C ∈ E ∧ A C ∈ E
218 biid ⊢ B C ∈ E ↔ B C ∈ E
219 203 218 212 3anbi123i ⊢ B A ∈ E ∧ B C ∈ E ∧ A C ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
220 216 217 219 3bitri ⊢ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
221 215 220 bitr3i ⊢ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
222 208 214 221 3anbi123i ⊢ C A ∈ E ∧ B A ∈ E ∧ C B ∈ E ∧ A B ∈ E ∧ C B ∈ E ∧ A C ∈ E ∧ B C ∈ E ∧ A C ∈ E ∧ B A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
223 df-3an ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
224 anabs1 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
225 anidm ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
226 223 224 225 3bitri ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
227 199 222 226 3bitri ⊢ C A ∈ E ∧ C B ∈ E ∧ B A ∈ E ∧ B C ∈ E ∧ A B ∈ E ∧ A C ∈ E ∧ C B ∈ E ∧ C A ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ A C ∈ E ∧ A B ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
228 180 227 syl6bb ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x ∈ A B C x A x B ⊆ E ∧ ∃! x ∈ A B C x A x C ⊆ E ∧ ∃! x ∈ A B C x B x C ⊆ E ∧ ∃! x ∈ A B C x B x A ⊆ E ∧ ∃! x ∈ A B C x C x A ⊆ E ∧ ∃! x ∈ A B C x C x B ⊆ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
229 13 98 228 3bitrd ⊢ 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
230 229 ex ⊢ 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