Metamath Proof Explorer

Theorem frgr3vlem1

Description: Lemma 1 for frgr3v . (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frgr3v.v ⊢V=Vtx⁡G
frgr3v.e ⊢E=Edg⁡G
Assertion frgr3vlem1 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→∀x∀yx∈ABC∧xAxB⊆E∧y∈ABC∧yAyB⊆E→x=y

Proof

Step Hyp Ref Expression
1 frgr3v.v ⊢V=Vtx⁡G
2 frgr3v.e ⊢E=Edg⁡G
3 vex ⊢x∈V
4 3 eltp ⊢x∈ABC↔x=A∨x=B∨x=C
5 vex ⊢y∈V
6 5 eltp ⊢y∈ABC↔y=A∨y=B∨y=C
7 eqidd ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=A
8 7 a1i ⊢AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=A
9 8 a1i13 ⊢y=A→AAAB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=A
10 preq1 ⊢y=A→yA=AA
11 preq1 ⊢y=A→yB=AB
12 10 11 preq12d ⊢y=A→yAyB=AAAB
13 12 sseq1d ⊢y=A→yAyB⊆E↔AAAB⊆E
14 eqeq2 ⊢y=A→A=y↔A=A
15 14 imbi2d ⊢y=A→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=A
16 15 imbi2d ⊢y=A→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y↔AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=A
17 9 13 16 3imtr4d ⊢y=A→yAyB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
18 prex ⊢AA∈V
19 prex ⊢AB∈V
20 18 19 prss ⊢AA∈E∧AB∈E↔AAAB⊆E
21 2 usgredgne ⊢G∈USGraph∧AA∈E→A≠A
22 21 adantll ⊢V=ABC∧G∈USGraph∧AA∈E→A≠A
23 df-ne ⊢A≠A↔¬A=A
24 eqid ⊢A=A
25 24 pm2.24i ⊢¬A=A→A=B
26 23 25 sylbi ⊢A≠A→A=B
27 22 26 syl ⊢V=ABC∧G∈USGraph∧AA∈E→A=B
28 27 expcom ⊢AA∈E→V=ABC∧G∈USGraph→A=B
29 28 adantr ⊢AA∈E∧AB∈E→V=ABC∧G∈USGraph→A=B
30 20 29 sylbir ⊢AAAB⊆E→V=ABC∧G∈USGraph→A=B
31 30 com12 ⊢V=ABC∧G∈USGraph→AAAB⊆E→A=B
32 31 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→AAAB⊆E→A=B
33 32 com12 ⊢AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=B
34 33 2a1i ⊢y=B→BABB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=B
35 preq1 ⊢y=B→yA=BA
36 preq1 ⊢y=B→yB=BB
37 35 36 preq12d ⊢y=B→yAyB=BABB
38 37 sseq1d ⊢y=B→yAyB⊆E↔BABB⊆E
39 eqeq2 ⊢y=B→A=y↔A=B
40 39 imbi2d ⊢y=B→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=B
41 40 imbi2d ⊢y=B→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y↔AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=B
42 34 38 41 3imtr4d ⊢y=B→yAyB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
43 24 pm2.24i ⊢¬A=A→A=C
44 23 43 sylbi ⊢A≠A→A=C
45 22 44 syl ⊢V=ABC∧G∈USGraph∧AA∈E→A=C
46 45 expcom ⊢AA∈E→V=ABC∧G∈USGraph→A=C
47 46 adantr ⊢AA∈E∧AB∈E→V=ABC∧G∈USGraph→A=C
48 20 47 sylbir ⊢AAAB⊆E→V=ABC∧G∈USGraph→A=C
49 48 com12 ⊢V=ABC∧G∈USGraph→AAAB⊆E→A=C
50 49 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→AAAB⊆E→A=C
51 50 com12 ⊢AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=C
52 51 2a1i ⊢y=C→CACB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=C
53 preq1 ⊢y=C→yA=CA
54 preq1 ⊢y=C→yB=CB
55 53 54 preq12d ⊢y=C→yAyB=CACB
56 55 sseq1d ⊢y=C→yAyB⊆E↔CACB⊆E
57 eqeq2 ⊢y=C→A=y↔A=C
58 57 imbi2d ⊢y=C→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=C
59 58 imbi2d ⊢y=C→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y↔AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=C
60 52 56 59 3imtr4d ⊢y=C→yAyB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
61 17 42 60 3jaoi ⊢y=A∨y=B∨y=C→yAyB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
62 preq1 ⊢x=A→xA=AA
63 preq1 ⊢x=A→xB=AB
64 62 63 preq12d ⊢x=A→xAxB=AAAB
65 64 sseq1d ⊢x=A→xAxB⊆E↔AAAB⊆E
66 eqeq1 ⊢x=A→x=y↔A=y
67 66 imbi2d ⊢x=A→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
68 65 67 imbi12d ⊢x=A→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
69 68 imbi2d ⊢x=A→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔yAyB⊆E→AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→A=y
70 61 69 imbitrrid ⊢x=A→y=A∨y=B∨y=C→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
71 prex ⊢BA∈V
72 prex ⊢BB∈V
73 71 72 prss ⊢BA∈E∧BB∈E↔BABB⊆E
74 2 usgredgne ⊢G∈USGraph∧BB∈E→B≠B
75 74 adantll ⊢V=ABC∧G∈USGraph∧BB∈E→B≠B
76 df-ne ⊢B≠B↔¬B=B
77 eqid ⊢B=B
78 77 pm2.24i ⊢¬B=B→B=A
79 76 78 sylbi ⊢B≠B→B=A
80 75 79 syl ⊢V=ABC∧G∈USGraph∧BB∈E→B=A
81 80 expcom ⊢BB∈E→V=ABC∧G∈USGraph→B=A
82 81 adantl ⊢BA∈E∧BB∈E→V=ABC∧G∈USGraph→B=A
83 73 82 sylbir ⊢BABB⊆E→V=ABC∧G∈USGraph→B=A
84 83 com12 ⊢V=ABC∧G∈USGraph→BABB⊆E→B=A
85 84 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→BABB⊆E→B=A
86 85 com12 ⊢BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=A
87 86 2a1i ⊢y=A→AAAB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=A
88 eqeq2 ⊢y=A→B=y↔B=A
89 88 imbi2d ⊢y=A→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=A
90 89 imbi2d ⊢y=A→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y↔BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=A
91 87 13 90 3imtr4d ⊢y=A→yAyB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
92 eqidd ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=B
93 92 a1i ⊢BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=B
94 93 a1i13 ⊢y=B→BABB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=B
95 eqeq2 ⊢y=B→B=y↔B=B
96 95 imbi2d ⊢y=B→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=B
97 96 imbi2d ⊢y=B→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y↔BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=B
98 94 38 97 3imtr4d ⊢y=B→yAyB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
99 77 pm2.24i ⊢¬B=B→B=C
100 76 99 sylbi ⊢B≠B→B=C
101 75 100 syl ⊢V=ABC∧G∈USGraph∧BB∈E→B=C
102 101 expcom ⊢BB∈E→V=ABC∧G∈USGraph→B=C
103 102 adantl ⊢BA∈E∧BB∈E→V=ABC∧G∈USGraph→B=C
104 73 103 sylbir ⊢BABB⊆E→V=ABC∧G∈USGraph→B=C
105 104 com12 ⊢V=ABC∧G∈USGraph→BABB⊆E→B=C
106 105 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→BABB⊆E→B=C
107 106 com12 ⊢BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=C
108 107 2a1i ⊢y=C→CACB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=C
109 eqeq2 ⊢y=C→B=y↔B=C
110 109 imbi2d ⊢y=C→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=C
111 110 imbi2d ⊢y=C→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y↔BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=C
112 108 56 111 3imtr4d ⊢y=C→yAyB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
113 91 98 112 3jaoi ⊢y=A∨y=B∨y=C→yAyB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
114 preq1 ⊢x=B→xA=BA
115 preq1 ⊢x=B→xB=BB
116 114 115 preq12d ⊢x=B→xAxB=BABB
117 116 sseq1d ⊢x=B→xAxB⊆E↔BABB⊆E
118 eqeq1 ⊢x=B→x=y↔B=y
119 118 imbi2d ⊢x=B→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
120 117 119 imbi12d ⊢x=B→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
121 120 imbi2d ⊢x=B→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔yAyB⊆E→BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→B=y
122 113 121 imbitrrid ⊢x=B→y=A∨y=B∨y=C→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
123 24 pm2.24i ⊢¬A=A→C=A
124 23 123 sylbi ⊢A≠A→C=A
125 22 124 syl ⊢V=ABC∧G∈USGraph∧AA∈E→C=A
126 125 expcom ⊢AA∈E→V=ABC∧G∈USGraph→C=A
127 126 adantr ⊢AA∈E∧AB∈E→V=ABC∧G∈USGraph→C=A
128 20 127 sylbir ⊢AAAB⊆E→V=ABC∧G∈USGraph→C=A
129 128 com12 ⊢V=ABC∧G∈USGraph→AAAB⊆E→C=A
130 129 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→AAAB⊆E→C=A
131 130 com12 ⊢AAAB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=A
132 131 a1i13 ⊢y=A→AAAB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=A
133 eqeq2 ⊢y=A→C=y↔C=A
134 133 imbi2d ⊢y=A→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=A
135 134 imbi2d ⊢y=A→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y↔CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=A
136 132 13 135 3imtr4d ⊢y=A→yAyB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
137 pm2.21 ⊢¬B=B→B=B→A∈X∧B∈Y∧C∈Z→C=B
138 76 137 sylbi ⊢B≠B→B=B→A∈X∧B∈Y∧C∈Z→C=B
139 75 77 138 mpisyl ⊢V=ABC∧G∈USGraph∧BB∈E→A∈X∧B∈Y∧C∈Z→C=B
140 139 expcom ⊢BB∈E→V=ABC∧G∈USGraph→A∈X∧B∈Y∧C∈Z→C=B
141 140 adantl ⊢BA∈E∧BB∈E→V=ABC∧G∈USGraph→A∈X∧B∈Y∧C∈Z→C=B
142 73 141 sylbir ⊢BABB⊆E→V=ABC∧G∈USGraph→A∈X∧B∈Y∧C∈Z→C=B
143 142 com13 ⊢A∈X∧B∈Y∧C∈Z→V=ABC∧G∈USGraph→BABB⊆E→C=B
144 143 a1d ⊢A∈X∧B∈Y∧C∈Z→A≠B∧A≠C∧B≠C→V=ABC∧G∈USGraph→BABB⊆E→C=B
145 144 3imp ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→BABB⊆E→C=B
146 145 com12 ⊢BABB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=B
147 146 a1i13 ⊢y=B→BABB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=B
148 eqeq2 ⊢y=B→C=y↔C=B
149 148 imbi2d ⊢y=B→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=B
150 149 imbi2d ⊢y=B→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y↔CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=B
151 147 38 150 3imtr4d ⊢y=B→yAyB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
152 eqidd ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=C
153 152 a1i ⊢CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=C
154 153 a1i13 ⊢y=C→CACB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=C
155 eqeq2 ⊢y=C→C=y↔C=C
156 155 imbi2d ⊢y=C→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=C
157 156 imbi2d ⊢y=C→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y↔CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=C
158 154 56 157 3imtr4d ⊢y=C→yAyB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
159 136 151 158 3jaoi ⊢y=A∨y=B∨y=C→yAyB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
160 preq1 ⊢x=C→xA=CA
161 preq1 ⊢x=C→xB=CB
162 160 161 preq12d ⊢x=C→xAxB=CACB
163 162 sseq1d ⊢x=C→xAxB⊆E↔CACB⊆E
164 eqeq1 ⊢x=C→x=y↔C=y
165 164 imbi2d ⊢x=C→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
166 163 165 imbi12d ⊢x=C→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
167 166 imbi2d ⊢x=C→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y↔yAyB⊆E→CACB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→C=y
168 159 167 imbitrrid ⊢x=C→y=A∨y=B∨y=C→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
169 70 122 168 3jaoi ⊢x=A∨x=B∨x=C→y=A∨y=B∨y=C→yAyB⊆E→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
170 169 com3l ⊢y=A∨y=B∨y=C→yAyB⊆E→x=A∨x=B∨x=C→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
171 6 170 sylbi ⊢y∈ABC→yAyB⊆E→x=A∨x=B∨x=C→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
172 171 imp ⊢y∈ABC∧yAyB⊆E→x=A∨x=B∨x=C→xAxB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
173 172 com3l ⊢x=A∨x=B∨x=C→xAxB⊆E→y∈ABC∧yAyB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
174 4 173 sylbi ⊢x∈ABC→xAxB⊆E→y∈ABC∧yAyB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
175 174 imp31 ⊢x∈ABC∧xAxB⊆E∧y∈ABC∧yAyB⊆E→A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x=y
176 175 com12 ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→x∈ABC∧xAxB⊆E∧y∈ABC∧yAyB⊆E→x=y
177 176 alrimivv ⊢A∈X∧B∈Y∧C∈Z∧A≠B∧A≠C∧B≠C∧V=ABC∧G∈USGraph→∀x∀yx∈ABC∧xAxB⊆E∧y∈ABC∧yAyB⊆E→x=y