Metamath Proof Explorer

Theorem 3vfriswmgrlem

Description: Lemma for 3vfriswmgr . (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ⊢ V = Vtx ⁡ G
3vfriswmgr.e ⊢ E = Edg ⁡ G
Assertion 3vfriswmgrlem ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph → A B ∈ E → ∃! w ∈ A B A w ∈ E

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ V = Vtx ⁡ G
2 3vfriswmgr.e ⊢ E = Edg ⁡ G
3 animorr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A A ∈ E ∨ A B ∈ E
4 preq2 ⊢ w = A → A w = A A
5 4 eleq1d ⊢ w = A → A w ∈ E ↔ A A ∈ E
6 preq2 ⊢ w = B → A w = A B
7 6 eleq1d ⊢ w = B → A w ∈ E ↔ A B ∈ E
8 5 7 rexprg ⊢ A ∈ X ∧ B ∈ Y → ∃ w ∈ A B A w ∈ E ↔ A A ∈ E ∨ A B ∈ E
9 8 3adant3 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → ∃ w ∈ A B A w ∈ E ↔ A A ∈ E ∨ A B ∈ E
10 9 ad2antrr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∃ w ∈ A B A w ∈ E ↔ A A ∈ E ∨ A B ∈ E
11 3 10 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∃ w ∈ A B A w ∈ E
12 df-rex ⊢ ∃ w ∈ A B A w ∈ E ↔ ∃ w w ∈ A B ∧ A w ∈ E
13 11 12 sylib ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∃ w w ∈ A B ∧ A w ∈ E
14 vex ⊢ w ∈ V
15 14 elpr ⊢ w ∈ A B ↔ w = A ∨ w = B
16 vex ⊢ y ∈ V
17 16 elpr ⊢ y ∈ A B ↔ y = A ∨ y = B
18 eqidd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = A
19 18 a1i ⊢ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = A
20 19 a1i13 ⊢ y = A → A A ∈ E → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = A
21 preq2 ⊢ y = A → A y = A A
22 21 eleq1d ⊢ y = A → A y ∈ E ↔ A A ∈ E
23 eqeq2 ⊢ y = A → A = y ↔ A = A
24 23 imbi2d ⊢ y = A → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y ↔ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = A
25 24 imbi2d ⊢ y = A → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y ↔ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = A
26 20 22 25 3imtr4d ⊢ y = A → A y ∈ E → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y
27 2 usgredgne ⊢ G ∈ USGraph ∧ A A ∈ E → A ≠ A
28 27 adantll ⊢ V = A B C ∧ G ∈ USGraph ∧ A A ∈ E → A ≠ A
29 df-ne ⊢ A ≠ A ↔ ¬ A = A
30 eqid ⊢ A = A
31 30 pm2.24i ⊢ ¬ A = A → A = B
32 29 31 sylbi ⊢ A ≠ A → A = B
33 28 32 syl ⊢ V = A B C ∧ G ∈ USGraph ∧ A A ∈ E → A = B
34 33 ex ⊢ V = A B C ∧ G ∈ USGraph → A A ∈ E → A = B
35 34 ad2antlr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A A ∈ E → A = B
36 35 com12 ⊢ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = B
37 36 2a1i ⊢ y = B → A B ∈ E → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = B
38 preq2 ⊢ y = B → A y = A B
39 38 eleq1d ⊢ y = B → A y ∈ E ↔ A B ∈ E
40 eqeq2 ⊢ y = B → A = y ↔ A = B
41 40 imbi2d ⊢ y = B → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y ↔ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = B
42 41 imbi2d ⊢ y = B → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y ↔ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = B
43 37 39 42 3imtr4d ⊢ y = B → A y ∈ E → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y
44 26 43 jaoi ⊢ y = A ∨ y = B → A y ∈ E → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y
45 eqeq1 ⊢ w = A → w = y ↔ A = y
46 45 imbi2d ⊢ w = A → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y ↔ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y
47 5 46 imbi12d ⊢ w = A → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y ↔ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y
48 47 imbi2d ⊢ w = A → A y ∈ E → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y ↔ A y ∈ E → A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A = y
49 44 48 syl5ibr ⊢ w = A → y = A ∨ y = B → A y ∈ E → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
50 30 pm2.24i ⊢ ¬ A = A → B = A
51 29 50 sylbi ⊢ A ≠ A → B = A
52 28 51 syl ⊢ V = A B C ∧ G ∈ USGraph ∧ A A ∈ E → B = A
53 52 ex ⊢ V = A B C ∧ G ∈ USGraph → A A ∈ E → B = A
54 53 ad2antlr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → A A ∈ E → B = A
55 54 com12 ⊢ A A ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = A
56 55 a1i13 ⊢ y = A → A A ∈ E → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = A
57 eqeq2 ⊢ y = A → B = y ↔ B = A
58 57 imbi2d ⊢ y = A → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y ↔ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = A
59 58 imbi2d ⊢ y = A → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y ↔ A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = A
60 56 22 59 3imtr4d ⊢ y = A → A y ∈ E → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y
61 eqidd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = B
62 61 a1i ⊢ A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = B
63 62 a1i13 ⊢ y = B → A B ∈ E → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = B
64 eqeq2 ⊢ y = B → B = y ↔ B = B
65 64 imbi2d ⊢ y = B → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y ↔ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = B
66 65 imbi2d ⊢ y = B → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y ↔ A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = B
67 63 39 66 3imtr4d ⊢ y = B → A y ∈ E → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y
68 60 67 jaoi ⊢ y = A ∨ y = B → A y ∈ E → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y
69 eqeq1 ⊢ w = B → w = y ↔ B = y
70 69 imbi2d ⊢ w = B → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y ↔ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y
71 7 70 imbi12d ⊢ w = B → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y ↔ A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y
72 71 imbi2d ⊢ w = B → A y ∈ E → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y ↔ A y ∈ E → A B ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → B = y
73 68 72 syl5ibr ⊢ w = B → y = A ∨ y = B → A y ∈ E → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
74 49 73 jaoi ⊢ w = A ∨ w = B → y = A ∨ y = B → A y ∈ E → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
75 74 com3l ⊢ y = A ∨ y = B → A y ∈ E → w = A ∨ w = B → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
76 17 75 sylbi ⊢ y ∈ A B → A y ∈ E → w = A ∨ w = B → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
77 76 imp ⊢ y ∈ A B ∧ A y ∈ E → w = A ∨ w = B → A w ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
78 77 com3l ⊢ w = A ∨ w = B → A w ∈ E → y ∈ A B ∧ A y ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
79 15 78 sylbi ⊢ w ∈ A B → A w ∈ E → y ∈ A B ∧ A y ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
80 79 imp31 ⊢ w ∈ A B ∧ A w ∈ E ∧ y ∈ A B ∧ A y ∈ E → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w = y
81 80 com12 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → w ∈ A B ∧ A w ∈ E ∧ y ∈ A B ∧ A y ∈ E → w = y
82 81 alrimivv ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∀ w ∀ y w ∈ A B ∧ A w ∈ E ∧ y ∈ A B ∧ A y ∈ E → w = y
83 eleq1w ⊢ w = y → w ∈ A B ↔ y ∈ A B
84 preq2 ⊢ w = y → A w = A y
85 84 eleq1d ⊢ w = y → A w ∈ E ↔ A y ∈ E
86 83 85 anbi12d ⊢ w = y → w ∈ A B ∧ A w ∈ E ↔ y ∈ A B ∧ A y ∈ E
87 86 eu4 ⊢ ∃! w w ∈ A B ∧ A w ∈ E ↔ ∃ w w ∈ A B ∧ A w ∈ E ∧ ∀ w ∀ y w ∈ A B ∧ A w ∈ E ∧ y ∈ A B ∧ A y ∈ E → w = y
88 13 82 87 sylanbrc ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∃! w w ∈ A B ∧ A w ∈ E
89 df-reu ⊢ ∃! w ∈ A B A w ∈ E ↔ ∃! w w ∈ A B ∧ A w ∈ E
90 88 89 sylibr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph ∧ A B ∈ E → ∃! w ∈ A B A w ∈ E
91 90 ex ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ V = A B C ∧ G ∈ USGraph → A B ∈ E → ∃! w ∈ A B A w ∈ E