Metamath Proof Explorer

Theorem isomuspgrlem2d

Description: Lemma 4 for isomuspgrlem2 . (Contributed by AV, 1-Dec-2022)

Ref Expression
Hypotheses isomushgr.v ⊢V=Vtx⁡A
isomushgr.w ⊢W=Vtx⁡B
isomushgr.e ⊢E=Edg⁡A
isomushgr.k ⊢K=Edg⁡B
isomuspgrlem2.g ⊢G=x∈E⟼Fx
isomuspgrlem2.a ⊢φ→A∈USHGraph
isomuspgrlem2.f ⊢φ→F:V⟶1-1 ontoW
isomuspgrlem2.i ⊢φ→∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K
isomuspgrlem2.x ⊢φ→F∈X
isomuspgrlem2.b ⊢φ→B∈USHGraph
Assertion isomuspgrlem2d ⊢φ→G:E⟶ontoK

Proof

Step Hyp Ref Expression
1 isomushgr.v ⊢V=Vtx⁡A
2 isomushgr.w ⊢W=Vtx⁡B
3 isomushgr.e ⊢E=Edg⁡A
4 isomushgr.k ⊢K=Edg⁡B
5 isomuspgrlem2.g ⊢G=x∈E⟼Fx
6 isomuspgrlem2.a ⊢φ→A∈USHGraph
7 isomuspgrlem2.f ⊢φ→F:V⟶1-1 ontoW
8 isomuspgrlem2.i ⊢φ→∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K
9 isomuspgrlem2.x ⊢φ→F∈X
10 isomuspgrlem2.b ⊢φ→B∈USHGraph
11 1 2 3 4 5 6 7 8 isomuspgrlem2b ⊢φ→G:E⟶K
12 uspgrupgr ⊢B∈USHGraph→B∈UPGraph
13 10 12 syl ⊢φ→B∈UPGraph
14 2 4 upgredg ⊢B∈UPGraph∧y∈K→∃c∈W∃d∈Wy=cd
15 13 14 sylan ⊢φ∧y∈K→∃c∈W∃d∈Wy=cd
16 eleq1 ⊢y=cd→y∈K↔cd∈K
17 16 anbi2d ⊢y=cd→φ∧y∈K↔φ∧cd∈K
18 f1ofo ⊢F:V⟶1-1 ontoW→F:V⟶ontoW
19 7 18 syl ⊢φ→F:V⟶ontoW
20 foelrn ⊢F:V⟶ontoW∧c∈W→∃m∈Vc=F⁡m
21 19 20 sylan ⊢φ∧c∈W→∃m∈Vc=F⁡m
22 21 ex ⊢φ→c∈W→∃m∈Vc=F⁡m
23 foelrn ⊢F:V⟶ontoW∧d∈W→∃n∈Vd=F⁡n
24 19 23 sylan ⊢φ∧d∈W→∃n∈Vd=F⁡n
25 24 ex ⊢φ→d∈W→∃n∈Vd=F⁡n
26 22 25 anim12d ⊢φ→c∈W∧d∈W→∃m∈Vc=F⁡m∧∃n∈Vd=F⁡n
27 26 adantr ⊢φ∧cd∈K→c∈W∧d∈W→∃m∈Vc=F⁡m∧∃n∈Vd=F⁡n
28 27 imp ⊢φ∧cd∈K∧c∈W∧d∈W→∃m∈Vc=F⁡m∧∃n∈Vd=F⁡n
29 preq12 ⊢c=F⁡m∧d=F⁡n→cd=F⁡mF⁡n
30 29 ancoms ⊢d=F⁡n∧c=F⁡m→cd=F⁡mF⁡n
31 30 eleq1d ⊢d=F⁡n∧c=F⁡m→cd∈K↔F⁡mF⁡n∈K
32 preq1 ⊢a=m→ab=mb
33 32 eleq1d ⊢a=m→ab∈E↔mb∈E
34 fveq2 ⊢a=m→F⁡a=F⁡m
35 34 preq1d ⊢a=m→F⁡aF⁡b=F⁡mF⁡b
36 35 eleq1d ⊢a=m→F⁡aF⁡b∈K↔F⁡mF⁡b∈K
37 33 36 bibi12d ⊢a=m→ab∈E↔F⁡aF⁡b∈K↔mb∈E↔F⁡mF⁡b∈K
38 preq2 ⊢b=n→mb=mn
39 38 eleq1d ⊢b=n→mb∈E↔mn∈E
40 fveq2 ⊢b=n→F⁡b=F⁡n
41 40 preq2d ⊢b=n→F⁡mF⁡b=F⁡mF⁡n
42 41 eleq1d ⊢b=n→F⁡mF⁡b∈K↔F⁡mF⁡n∈K
43 39 42 bibi12d ⊢b=n→mb∈E↔F⁡mF⁡b∈K↔mn∈E↔F⁡mF⁡n∈K
44 37 43 rspc2va ⊢m∈V∧n∈V∧∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K→mn∈E↔F⁡mF⁡n∈K
45 44 bicomd ⊢m∈V∧n∈V∧∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K→F⁡mF⁡n∈K↔mn∈E
46 45 ancoms ⊢∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K∧m∈V∧n∈V→F⁡mF⁡n∈K↔mn∈E
47 46 biimpd ⊢∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K∧m∈V∧n∈V→F⁡mF⁡n∈K→mn∈E
48 47 ex ⊢∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K→m∈V∧n∈V→F⁡mF⁡n∈K→mn∈E
49 8 48 syl ⊢φ→m∈V∧n∈V→F⁡mF⁡n∈K→mn∈E
50 49 com13 ⊢F⁡mF⁡n∈K→m∈V∧n∈V→φ→mn∈E
51 31 50 syl6bi ⊢d=F⁡n∧c=F⁡m→cd∈K→m∈V∧n∈V→φ→mn∈E
52 51 com14 ⊢φ→cd∈K→m∈V∧n∈V→d=F⁡n∧c=F⁡m→mn∈E
53 52 imp ⊢φ∧cd∈K→m∈V∧n∈V→d=F⁡n∧c=F⁡m→mn∈E
54 53 adantr ⊢φ∧cd∈K∧c∈W∧d∈W→m∈V∧n∈V→d=F⁡n∧c=F⁡m→mn∈E
55 54 imp31 ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m→mn∈E
56 imaeq2 ⊢e=mn→Fe=Fmn
57 f1ofn ⊢F:V⟶1-1 ontoW→FFnV
58 7 57 syl ⊢φ→FFnV
59 58 ad3antrrr ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→FFnV
60 simprl ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→m∈V
61 simpr ⊢m∈V∧n∈V→n∈V
62 61 adantl ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→n∈V
63 59 60 62 3jca ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→FFnV∧m∈V∧n∈V
64 63 adantr ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m→FFnV∧m∈V∧n∈V
65 fnimapr ⊢FFnV∧m∈V∧n∈V→Fmn=F⁡mF⁡n
66 64 65 syl ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m→Fmn=F⁡mF⁡n
67 56 66 sylan9eqr ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m∧e=mn→Fe=F⁡mF⁡n
68 67 eqeq2d ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m∧e=mn→cd=Fe↔cd=F⁡mF⁡n
69 30 adantl ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m→cd=F⁡mF⁡n
70 55 68 69 rspcedvd ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V∧d=F⁡n∧c=F⁡m→∃e∈Ecd=Fe
71 70 ex ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→d=F⁡n∧c=F⁡m→∃e∈Ecd=Fe
72 71 anassrs ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→d=F⁡n∧c=F⁡m→∃e∈Ecd=Fe
73 72 expd ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V∧n∈V→d=F⁡n→c=F⁡m→∃e∈Ecd=Fe
74 73 rexlimdva ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V→∃n∈Vd=F⁡n→c=F⁡m→∃e∈Ecd=Fe
75 74 com23 ⊢φ∧cd∈K∧c∈W∧d∈W∧m∈V→c=F⁡m→∃n∈Vd=F⁡n→∃e∈Ecd=Fe
76 75 rexlimdva ⊢φ∧cd∈K∧c∈W∧d∈W→∃m∈Vc=F⁡m→∃n∈Vd=F⁡n→∃e∈Ecd=Fe
77 76 impd ⊢φ∧cd∈K∧c∈W∧d∈W→∃m∈Vc=F⁡m∧∃n∈Vd=F⁡n→∃e∈Ecd=Fe
78 28 77 mpd ⊢φ∧cd∈K∧c∈W∧d∈W→∃e∈Ecd=Fe
79 78 ex ⊢φ∧cd∈K→c∈W∧d∈W→∃e∈Ecd=Fe
80 17 79 syl6bi ⊢y=cd→φ∧y∈K→c∈W∧d∈W→∃e∈Ecd=Fe
81 80 impd ⊢y=cd→φ∧y∈K∧c∈W∧d∈W→∃e∈Ecd=Fe
82 81 impcom ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd→∃e∈Ecd=Fe
83 simpr ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd→y=cd
84 83 adantr ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd∧e∈E→y=cd
85 9 ad4antr ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd∧e∈E→F∈X
86 1 2 3 4 5 isomuspgrlem2a ⊢F∈X→∀y∈EFy=G⁡y
87 85 86 syl ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd∧e∈E→∀y∈EFy=G⁡y
88 imaeq2 ⊢y=e→Fy=Fe
89 fveq2 ⊢y=e→G⁡y=G⁡e
90 88 89 eqeq12d ⊢y=e→Fy=G⁡y↔Fe=G⁡e
91 90 rspcv ⊢e∈E→∀y∈EFy=G⁡y→Fe=G⁡e
92 eqcom ⊢G⁡e=Fe↔Fe=G⁡e
93 91 92 syl6ibr ⊢e∈E→∀y∈EFy=G⁡y→G⁡e=Fe
94 93 adantl ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd∧e∈E→∀y∈EFy=G⁡y→G⁡e=Fe
95 87 94 mpd ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd∧e∈E→G⁡e=Fe
96 84 95 eqeq12d ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd∧e∈E→y=G⁡e↔cd=Fe
97 96 rexbidva ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd→∃e∈Ey=G⁡e↔∃e∈Ecd=Fe
98 82 97 mpbird ⊢φ∧y∈K∧c∈W∧d∈W∧y=cd→∃e∈Ey=G⁡e
99 98 ex ⊢φ∧y∈K∧c∈W∧d∈W→y=cd→∃e∈Ey=G⁡e
100 99 rexlimdvva ⊢φ∧y∈K→∃c∈W∃d∈Wy=cd→∃e∈Ey=G⁡e
101 15 100 mpd ⊢φ∧y∈K→∃e∈Ey=G⁡e
102 101 ralrimiva ⊢φ→∀y∈K∃e∈Ey=G⁡e
103 dffo3 ⊢G:E⟶ontoK↔G:E⟶K∧∀y∈K∃e∈Ey=G⁡e
104 11 102 103 sylanbrc ⊢φ→G:E⟶ontoK