Metamath Proof Explorer

Theorem isomuspgrlem2b

Description: Lemma 2 for isomuspgrlem2 . (Contributed by AV, 29-Nov-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
Assertion isomuspgrlem2b ⊢φ→G:E⟶K

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 uspgrupgr ⊢A∈USHGraph→A∈UPGraph
10 6 9 syl ⊢φ→A∈UPGraph
11 1 3 upgredg ⊢A∈UPGraph∧x∈E→∃c∈V∃d∈Vx=cd
12 10 11 sylan ⊢φ∧x∈E→∃c∈V∃d∈Vx=cd
13 preq12 ⊢a=c∧b=d→ab=cd
14 13 eleq1d ⊢a=c∧b=d→ab∈E↔cd∈E
15 fveq2 ⊢a=c→F⁡a=F⁡c
16 15 adantr ⊢a=c∧b=d→F⁡a=F⁡c
17 fveq2 ⊢b=d→F⁡b=F⁡d
18 17 adantl ⊢a=c∧b=d→F⁡b=F⁡d
19 16 18 preq12d ⊢a=c∧b=d→F⁡aF⁡b=F⁡cF⁡d
20 19 eleq1d ⊢a=c∧b=d→F⁡aF⁡b∈K↔F⁡cF⁡d∈K
21 14 20 bibi12d ⊢a=c∧b=d→ab∈E↔F⁡aF⁡b∈K↔cd∈E↔F⁡cF⁡d∈K
22 21 rspc2gv ⊢c∈V∧d∈V→∀a∈V∀b∈Vab∈E↔F⁡aF⁡b∈K→cd∈E↔F⁡cF⁡d∈K
23 8 22 syl5com ⊢φ→c∈V∧d∈V→cd∈E↔F⁡cF⁡d∈K
24 23 adantr ⊢φ∧x=cd→c∈V∧d∈V→cd∈E↔F⁡cF⁡d∈K
25 24 imp ⊢φ∧x=cd∧c∈V∧d∈V→cd∈E↔F⁡cF⁡d∈K
26 bicom ⊢cd∈E↔F⁡cF⁡d∈K↔F⁡cF⁡d∈K↔cd∈E
27 bianir ⊢cd∈E∧F⁡cF⁡d∈K↔cd∈E→F⁡cF⁡d∈K
28 27 ex ⊢cd∈E→F⁡cF⁡d∈K↔cd∈E→F⁡cF⁡d∈K
29 26 28 biimtrid ⊢cd∈E→cd∈E↔F⁡cF⁡d∈K→F⁡cF⁡d∈K
30 f1ofn ⊢F:V⟶1-1 ontoW→FFnV
31 7 30 syl ⊢φ→FFnV
32 31 adantr ⊢φ∧x=cd→FFnV
33 32 adantr ⊢φ∧x=cd∧c∈V∧d∈V→FFnV
34 simprl ⊢φ∧x=cd∧c∈V∧d∈V→c∈V
35 simprr ⊢φ∧x=cd∧c∈V∧d∈V→d∈V
36 33 34 35 3jca ⊢φ∧x=cd∧c∈V∧d∈V→FFnV∧c∈V∧d∈V
37 36 adantl ⊢cd∈E∧φ∧x=cd∧c∈V∧d∈V→FFnV∧c∈V∧d∈V
38 fnimapr ⊢FFnV∧c∈V∧d∈V→Fcd=F⁡cF⁡d
39 37 38 syl ⊢cd∈E∧φ∧x=cd∧c∈V∧d∈V→Fcd=F⁡cF⁡d
40 39 eqcomd ⊢cd∈E∧φ∧x=cd∧c∈V∧d∈V→F⁡cF⁡d=Fcd
41 40 eleq1d ⊢cd∈E∧φ∧x=cd∧c∈V∧d∈V→F⁡cF⁡d∈K↔Fcd∈K
42 41 biimpd ⊢cd∈E∧φ∧x=cd∧c∈V∧d∈V→F⁡cF⁡d∈K→Fcd∈K
43 42 ex ⊢cd∈E→φ∧x=cd∧c∈V∧d∈V→F⁡cF⁡d∈K→Fcd∈K
44 43 com23 ⊢cd∈E→F⁡cF⁡d∈K→φ∧x=cd∧c∈V∧d∈V→Fcd∈K
45 29 44 syld ⊢cd∈E→cd∈E↔F⁡cF⁡d∈K→φ∧x=cd∧c∈V∧d∈V→Fcd∈K
46 45 com13 ⊢φ∧x=cd∧c∈V∧d∈V→cd∈E↔F⁡cF⁡d∈K→cd∈E→Fcd∈K
47 25 46 mpd ⊢φ∧x=cd∧c∈V∧d∈V→cd∈E→Fcd∈K
48 eleq1 ⊢x=cd→x∈E↔cd∈E
49 imaeq2 ⊢x=cd→Fx=Fcd
50 49 eleq1d ⊢x=cd→Fx∈K↔Fcd∈K
51 48 50 imbi12d ⊢x=cd→x∈E→Fx∈K↔cd∈E→Fcd∈K
52 51 adantl ⊢φ∧x=cd→x∈E→Fx∈K↔cd∈E→Fcd∈K
53 52 adantr ⊢φ∧x=cd∧c∈V∧d∈V→x∈E→Fx∈K↔cd∈E→Fcd∈K
54 47 53 mpbird ⊢φ∧x=cd∧c∈V∧d∈V→x∈E→Fx∈K
55 54 exp31 ⊢φ→x=cd→c∈V∧d∈V→x∈E→Fx∈K
56 55 com24 ⊢φ→x∈E→c∈V∧d∈V→x=cd→Fx∈K
57 56 imp31 ⊢φ∧x∈E∧c∈V∧d∈V→x=cd→Fx∈K
58 57 rexlimdvva ⊢φ∧x∈E→∃c∈V∃d∈Vx=cd→Fx∈K
59 12 58 mpd ⊢φ∧x∈E→Fx∈K
60 59 ralrimiva ⊢φ→∀x∈EFx∈K
61 5 fmpt ⊢∀x∈EFx∈K↔G:E⟶K
62 60 61 sylib ⊢φ→G:E⟶K