Metamath Proof Explorer

Theorem frgr3vlem2

Description: Lemma 2 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 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

Proof

Step Hyp Ref Expression
1 frgr3v.v ⊢ V = Vtx ⁡ G
2 frgr3v.e ⊢ E = Edg ⁡ G
3 df-reu ⊢ ∃! x ∈ A B C x A x B ⊆ E ↔ ∃! x x ∈ A B C ∧ x A x B ⊆ E
4 eleq1w ⊢ x = y → x ∈ A B C ↔ y ∈ A B C
5 preq1 ⊢ x = y → x A = y A
6 preq1 ⊢ x = y → x B = y B
7 5 6 preq12d ⊢ x = y → x A x B = y A y B
8 7 sseq1d ⊢ x = y → x A x B ⊆ E ↔ y A y B ⊆ E
9 4 8 anbi12d ⊢ x = y → x ∈ A B C ∧ x A x B ⊆ E ↔ y ∈ A B C ∧ y A y B ⊆ E
10 9 eu4 ⊢ ∃! x x ∈ A B C ∧ x A x B ⊆ E ↔ ∃ x x ∈ A B C ∧ x A x B ⊆ E ∧ ∀ x ∀ y x ∈ A B C ∧ x A x B ⊆ E ∧ y ∈ A B C ∧ y A y B ⊆ E → x = y
11 1 2 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
12 11 3expa ⊢ 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
13 12 biantrud ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃ x x ∈ A B C ∧ x A x B ⊆ E ↔ ∃ x x ∈ A B C ∧ x A x B ⊆ E ∧ ∀ x ∀ y x ∈ A B C ∧ x A x B ⊆ E ∧ y ∈ A B C ∧ y A y B ⊆ E → x = y
14 vex ⊢ x ∈ V
15 14 eltp ⊢ x ∈ A B C ↔ x = A ∨ x = B ∨ x = C
16 preq1 ⊢ x = A → x A = A A
17 preq1 ⊢ x = A → x B = A B
18 16 17 preq12d ⊢ x = A → x A x B = A A A B
19 18 sseq1d ⊢ x = A → x A x B ⊆ E ↔ A A A B ⊆ E
20 prex ⊢ A A ∈ V
21 prex ⊢ A B ∈ V
22 20 21 prss ⊢ A A ∈ E ∧ A B ∈ E ↔ A A A B ⊆ E
23 2 usgredgne ⊢ G ∈ USGraph ∧ A A ∈ E → A ≠ A
24 23 adantll ⊢ V = A B C ∧ G ∈ USGraph ∧ A A ∈ E → A ≠ A
25 df-ne ⊢ A ≠ A ↔ ¬ A = A
26 eqid ⊢ A = A
27 26 pm2.24i ⊢ ¬ A = A → C A ∈ E ∧ C B ∈ E
28 25 27 sylbi ⊢ A ≠ A → C A ∈ E ∧ C B ∈ E
29 24 28 syl ⊢ V = A B C ∧ G ∈ USGraph ∧ A A ∈ E → C A ∈ E ∧ C B ∈ E
30 29 ex ⊢ V = A B C ∧ G ∈ USGraph → A A ∈ E → C A ∈ E ∧ C B ∈ E
31 30 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → A A ∈ E → C A ∈ E ∧ C B ∈ E
32 31 com12 ⊢ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
33 32 adantr ⊢ A A ∈ E ∧ A B ∈ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
34 22 33 sylbir ⊢ 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 ∈ E ∧ C B ∈ E
35 19 34 biimtrdi ⊢ 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 → C A ∈ E ∧ C B ∈ E
36 preq1 ⊢ x = B → x A = B A
37 preq1 ⊢ x = B → x B = B B
38 36 37 preq12d ⊢ x = B → x A x B = B A B B
39 38 sseq1d ⊢ x = B → x A x B ⊆ E ↔ B A B B ⊆ E
40 prex ⊢ B A ∈ V
41 prex ⊢ B B ∈ V
42 40 41 prss ⊢ B A ∈ E ∧ B B ∈ E ↔ B A B B ⊆ E
43 2 usgredgne ⊢ G ∈ USGraph ∧ B B ∈ E → B ≠ B
44 43 adantll ⊢ V = A B C ∧ G ∈ USGraph ∧ B B ∈ E → B ≠ B
45 df-ne ⊢ B ≠ B ↔ ¬ B = B
46 eqid ⊢ B = B
47 46 pm2.24i ⊢ ¬ B = B → C A ∈ E ∧ C B ∈ E
48 45 47 sylbi ⊢ B ≠ B → C A ∈ E ∧ C B ∈ E
49 44 48 syl ⊢ V = A B C ∧ G ∈ USGraph ∧ B B ∈ E → C A ∈ E ∧ C B ∈ E
50 49 ex ⊢ V = A B C ∧ G ∈ USGraph → B B ∈ E → C A ∈ E ∧ C B ∈ E
51 50 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → B B ∈ E → C A ∈ E ∧ C B ∈ E
52 51 com12 ⊢ B B ∈ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
53 52 adantl ⊢ B A ∈ E ∧ B B ∈ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
54 42 53 sylbir ⊢ B A B B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
55 39 54 biimtrdi ⊢ 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 → C A ∈ E ∧ C B ∈ E
56 preq1 ⊢ x = C → x A = C A
57 preq1 ⊢ x = C → x B = C B
58 56 57 preq12d ⊢ x = C → x A x B = C A C B
59 58 sseq1d ⊢ x = C → x A x B ⊆ E ↔ C A C B ⊆ E
60 prex ⊢ C A ∈ V
61 prex ⊢ C B ∈ V
62 60 61 prss ⊢ C A ∈ E ∧ C B ∈ E ↔ C A C B ⊆ E
63 ax-1 ⊢ C A ∈ E ∧ C B ∈ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
64 62 63 sylbir ⊢ 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 ∈ E ∧ C B ∈ E
65 59 64 biimtrdi ⊢ 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 → C A ∈ E ∧ C B ∈ E
66 35 55 65 3jaoi ⊢ 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 → C A ∈ E ∧ C B ∈ E
67 15 66 sylbi ⊢ x ∈ A B C → x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
68 67 imp ⊢ x ∈ A B C ∧ x A x B ⊆ E → A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E
69 68 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 → C A ∈ E ∧ C B ∈ E
70 69 exlimdv ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃ x x ∈ A B C ∧ x A x B ⊆ E → C A ∈ E ∧ C B ∈ E
71 prssi ⊢ C A ∈ E ∧ C B ∈ E → C A C B ⊆ E
72 71 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ C A ∈ E ∧ C B ∈ E → C A C B ⊆ E
73 72 3mix3d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ C A ∈ E ∧ C B ∈ E → A A A B ⊆ E ∨ B A B B ⊆ E ∨ C A C B ⊆ E
74 19 39 59 rextpg ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ x ∈ A B C x A x B ⊆ E ↔ A A A B ⊆ E ∨ B A B B ⊆ E ∨ C A C B ⊆ E
75 74 ad3antrrr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ C A ∈ E ∧ C B ∈ E → ∃ x ∈ A B C x A x B ⊆ E ↔ A A A B ⊆ E ∨ B A B B ⊆ E ∨ C A C B ⊆ E
76 73 75 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ C A ∈ E ∧ C B ∈ E → ∃ x ∈ A B C x A x B ⊆ E
77 df-rex ⊢ ∃ x ∈ A B C x A x B ⊆ E ↔ ∃ x x ∈ A B C ∧ x A x B ⊆ E
78 76 77 sylib ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph ∧ C A ∈ E ∧ C B ∈ E → ∃ x x ∈ A B C ∧ x A x B ⊆ E
79 78 ex ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → C A ∈ E ∧ C B ∈ E → ∃ x x ∈ A B C ∧ x A x B ⊆ E
80 70 79 impbid ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃ x x ∈ A B C ∧ x A x B ⊆ E ↔ C A ∈ E ∧ C B ∈ E
81 13 80 bitr3d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃ x x ∈ A B C ∧ x A x B ⊆ E ∧ ∀ x ∀ y x ∈ A B C ∧ x A x B ⊆ E ∧ y ∈ A B C ∧ y A y B ⊆ E → x = y ↔ C A ∈ E ∧ C B ∈ E
82 10 81 bitrid ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ V = A B C ∧ G ∈ USGraph → ∃! x x ∈ A B C ∧ x A x B ⊆ E ↔ C A ∈ E ∧ C B ∈ E
83 3 82 bitrid ⊢ 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
84 83 ex ⊢ 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