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 = A B C ∧ G ∈ USGraph → ∀ x ∀ y x ∈ A B C ∧ x A x B ⊆ E ∧ y ∈ A B C ∧ y A y B ⊆ 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 ∈ A B C ↔ x = A ∨ x = B ∨ x = C
5 vex ⊢ y ∈ V
6 5 eltp ⊢ y ∈ A B C ↔ y = A ∨ y = B ∨ y = C
7 eqidd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = A
8 7 a1i ⊢ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = A
9 8 a1i13 ⊢ y = A → A A A B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = A
10 preq1 ⊢ y = A → y A = A A
11 preq1 ⊢ y = A → y B = A B
12 10 11 preq12d ⊢ y = A → y A y B = A A A B
13 12 sseq1d ⊢ y = A → y A y B ⊆ E ↔ A A A B ⊆ 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 = A B C ∧ G ∈ USGraph → A = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = A
16 15 imbi2d ⊢ y = A → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y ↔ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = A
17 9 13 16 3imtr4d ⊢ y = A → y A y B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y
18 prex ⊢ A A ∈ V
19 prex ⊢ A B ∈ V
20 18 19 prss ⊢ A A ∈ E ∧ A B ∈ E ↔ A A A B ⊆ E
21 2 usgredgne ⊢ G ∈ USGraph ∧ A A ∈ E → A ≠ A
22 21 adantll ⊢ V = A B C ∧ G ∈ USGraph ∧ A A ∈ 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 = A B C ∧ G ∈ USGraph ∧ A A ∈ E → A = B
28 27 expcom ⊢ A A ∈ E → V = A B C ∧ G ∈ USGraph → A = B
29 28 adantr ⊢ A A ∈ E ∧ A B ∈ E → V = A B C ∧ G ∈ USGraph → A = B
30 20 29 sylbir ⊢ A A A B ⊆ E → V = A B C ∧ G ∈ USGraph → A = B
31 30 com12 ⊢ V = A B C ∧ G ∈ USGraph → A A A B ⊆ E → A = B
32 31 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A A A B ⊆ E → A = B
33 32 com12 ⊢ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = B
34 33 2a1i ⊢ y = B → B A B B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = B
35 preq1 ⊢ y = B → y A = B A
36 preq1 ⊢ y = B → y B = B B
37 35 36 preq12d ⊢ y = B → y A y B = B A B B
38 37 sseq1d ⊢ y = B → y A y B ⊆ E ↔ B A B B ⊆ 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 = A B C ∧ G ∈ USGraph → A = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = B
41 40 imbi2d ⊢ y = B → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y ↔ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = B
42 34 38 41 3imtr4d ⊢ y = B → y A y B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph ∧ A A ∈ E → A = C
46 45 expcom ⊢ A A ∈ E → V = A B C ∧ G ∈ USGraph → A = C
47 46 adantr ⊢ A A ∈ E ∧ A B ∈ E → V = A B C ∧ G ∈ USGraph → A = C
48 20 47 sylbir ⊢ A A A B ⊆ E → V = A B C ∧ G ∈ USGraph → A = C
49 48 com12 ⊢ V = A B C ∧ G ∈ USGraph → A A A B ⊆ E → A = C
50 49 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A A A B ⊆ E → A = C
51 50 com12 ⊢ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = C
52 51 2a1i ⊢ y = C → C A C B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = C
53 preq1 ⊢ y = C → y A = C A
54 preq1 ⊢ y = C → y B = C B
55 53 54 preq12d ⊢ y = C → y A y B = C A C B
56 55 sseq1d ⊢ y = C → y A y B ⊆ E ↔ C A C B ⊆ 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 = A B C ∧ G ∈ USGraph → A = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = C
59 58 imbi2d ⊢ y = C → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y ↔ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = C
60 52 56 59 3imtr4d ⊢ y = C → y A y B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y
61 17 42 60 3jaoi ⊢ y = A ∨ y = B ∨ y = C → y A y B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y
62 preq1 ⊢ x = A → x A = A A
63 preq1 ⊢ x = A → x B = A B
64 62 63 preq12d ⊢ x = A → x A x B = A A A B
65 64 sseq1d ⊢ x = A → x A x B ⊆ E ↔ A A A B ⊆ 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 = A B C ∧ G ∈ USGraph → x = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y
68 65 67 imbi12d ⊢ x = A → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y ↔ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y
69 68 imbi2d ⊢ x = A → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y ↔ y A y B ⊆ E → A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A = y
70 61 69 syl5ibr ⊢ x = A → y = A ∨ y = B ∨ y = C → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
71 prex ⊢ B A ∈ V
72 prex ⊢ B B ∈ V
73 71 72 prss ⊢ B A ∈ E ∧ B B ∈ E ↔ B A B B ⊆ E
74 2 usgredgne ⊢ G ∈ USGraph ∧ B B ∈ E → B ≠ B
75 74 adantll ⊢ V = A B C ∧ G ∈ USGraph ∧ B B ∈ 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 = A B C ∧ G ∈ USGraph ∧ B B ∈ E → B = A
81 80 expcom ⊢ B B ∈ E → V = A B C ∧ G ∈ USGraph → B = A
82 81 adantl ⊢ B A ∈ E ∧ B B ∈ E → V = A B C ∧ G ∈ USGraph → B = A
83 73 82 sylbir ⊢ B A B B ⊆ E → V = A B C ∧ G ∈ USGraph → B = A
84 83 com12 ⊢ V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → B = A
85 84 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → B = A
86 85 com12 ⊢ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = A
87 86 2a1i ⊢ y = A → A A A B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph → B = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = A
90 89 imbi2d ⊢ y = A → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y ↔ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = A
91 87 13 90 3imtr4d ⊢ y = A → y A y B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y
92 eqidd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = B
93 92 a1i ⊢ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = B
94 93 a1i13 ⊢ y = B → B A B B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph → B = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = B
97 96 imbi2d ⊢ y = B → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y ↔ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = B
98 94 38 97 3imtr4d ⊢ y = B → y A y B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph ∧ B B ∈ E → B = C
102 101 expcom ⊢ B B ∈ E → V = A B C ∧ G ∈ USGraph → B = C
103 102 adantl ⊢ B A ∈ E ∧ B B ∈ E → V = A B C ∧ G ∈ USGraph → B = C
104 73 103 sylbir ⊢ B A B B ⊆ E → V = A B C ∧ G ∈ USGraph → B = C
105 104 com12 ⊢ V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → B = C
106 105 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → B = C
107 106 com12 ⊢ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = C
108 107 2a1i ⊢ y = C → C A C B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph → B = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = C
111 110 imbi2d ⊢ y = C → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y ↔ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = C
112 108 56 111 3imtr4d ⊢ y = C → y A y B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y
113 91 98 112 3jaoi ⊢ y = A ∨ y = B ∨ y = C → y A y B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y
114 preq1 ⊢ x = B → x A = B A
115 preq1 ⊢ x = B → x B = B B
116 114 115 preq12d ⊢ x = B → x A x B = B A B B
117 116 sseq1d ⊢ x = B → x A x B ⊆ E ↔ B A B B ⊆ 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 = A B C ∧ G ∈ USGraph → x = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y
120 117 119 imbi12d ⊢ x = B → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y ↔ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y
121 120 imbi2d ⊢ x = B → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y ↔ y A y B ⊆ E → B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B = y
122 113 121 syl5ibr ⊢ x = B → y = A ∨ y = B ∨ y = C → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph ∧ A A ∈ E → C = A
126 125 expcom ⊢ A A ∈ E → V = A B C ∧ G ∈ USGraph → C = A
127 126 adantr ⊢ A A ∈ E ∧ A B ∈ E → V = A B C ∧ G ∈ USGraph → C = A
128 20 127 sylbir ⊢ A A A B ⊆ E → V = A B C ∧ G ∈ USGraph → C = A
129 128 com12 ⊢ V = A B C ∧ G ∈ USGraph → A A A B ⊆ E → C = A
130 129 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A A A B ⊆ E → C = A
131 130 com12 ⊢ A A A B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = A
132 131 a1i13 ⊢ y = A → A A A B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph → C = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = A
135 134 imbi2d ⊢ y = A → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y ↔ C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = A
136 132 13 135 3imtr4d ⊢ y = A → y A y B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph ∧ B B ∈ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C = B
140 139 expcom ⊢ B B ∈ E → V = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C = B
141 140 adantl ⊢ B A ∈ E ∧ B B ∈ E → V = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C = B
142 73 141 sylbir ⊢ B A B B ⊆ E → V = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C = B
143 142 com13 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → C = B
144 143 a1d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → A ≠ B ∧ A ≠ C ∧ B ≠ C → V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → C = B
145 144 3imp ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B A B B ⊆ E → C = B
146 145 com12 ⊢ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = B
147 146 a1i13 ⊢ y = B → B A B B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph → C = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = B
150 149 imbi2d ⊢ y = B → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y ↔ C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = B
151 147 38 150 3imtr4d ⊢ y = B → y A y B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y
152 eqidd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = C
153 152 a1i ⊢ C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = C
154 153 a1i13 ⊢ y = C → C A C B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ 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 = A B C ∧ G ∈ USGraph → C = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = C
157 156 imbi2d ⊢ y = C → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y ↔ C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = C
158 154 56 157 3imtr4d ⊢ y = C → y A y B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y
159 136 151 158 3jaoi ⊢ y = A ∨ y = B ∨ y = C → y A y B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y
160 preq1 ⊢ x = C → x A = C A
161 preq1 ⊢ x = C → x B = C B
162 160 161 preq12d ⊢ x = C → x A x B = C A C B
163 162 sseq1d ⊢ x = C → x A x B ⊆ E ↔ C A C B ⊆ 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 = A B C ∧ G ∈ USGraph → x = y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y
166 163 165 imbi12d ⊢ x = C → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y ↔ C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y
167 166 imbi2d ⊢ x = C → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y ↔ y A y B ⊆ E → C A C B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C = y
168 159 167 syl5ibr ⊢ x = C → y = A ∨ y = B ∨ y = C → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
169 70 122 168 3jaoi ⊢ x = A ∨ x = B ∨ x = C → y = A ∨ y = B ∨ y = C → y A y B ⊆ E → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
170 169 com3l ⊢ y = A ∨ y = B ∨ y = C → y A y B ⊆ E → x = A ∨ x = B ∨ x = C → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
171 6 170 sylbi ⊢ y ∈ A B C → y A y B ⊆ E → x = A ∨ x = B ∨ x = C → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
172 171 imp ⊢ y ∈ A B C ∧ y A y B ⊆ E → x = A ∨ x = B ∨ x = C → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
173 172 com3l ⊢ x = A ∨ x = B ∨ x = C → x A x B ⊆ E → y ∈ A B C ∧ y A y B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
174 4 173 sylbi ⊢ x ∈ A B C → x A x B ⊆ E → y ∈ A B C ∧ y A y B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
175 174 imp31 ⊢ x ∈ A B C ∧ x A x B ⊆ E ∧ y ∈ A B C ∧ y A y B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → x = y
176 175 com12 ⊢ 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 ∧ y ∈ A B C ∧ y A y B ⊆ E → x = y
177 176 alrimivv ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∀ x ∀ y x ∈ A B C ∧ x A x B ⊆ E ∧ y ∈ A B C ∧ y A y B ⊆ E → x = y