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