Metamath Proof Explorer

Theorem isomuspgrlem2

Description: Lemma 2 for isomuspgr . (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
Assertion isomuspgrlem2 ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e

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 3 fvexi ⊢E∈V
6 5 mptex ⊢x∈E⟼fx∈V
7 eqid ⊢x∈E⟼fx=x∈E⟼fx
8 simplll ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→A∈USHGraph
9 simplr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→f:V⟶1-1 ontoW
10 simpr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
11 vex ⊢f∈V
12 11 a1i ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→f∈V
13 simpllr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→B∈USHGraph
14 1 2 3 4 7 8 9 10 12 13 isomuspgrlem2e ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→x∈E⟼fx:E⟶1-1 ontoK
15 1 2 3 4 7 isomuspgrlem2a ⊢f∈V→∀e∈Efe=x∈E⟼fx⁡e
16 11 15 mp1i ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→∀e∈Efe=x∈E⟼fx⁡e
17 14 16 jca ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→x∈E⟼fx:E⟶1-1 ontoK∧∀e∈Efe=x∈E⟼fx⁡e
18 f1oeq1 ⊢g=x∈E⟼fx→g:E⟶1-1 ontoK↔x∈E⟼fx:E⟶1-1 ontoK
19 fveq1 ⊢g=x∈E⟼fx→g⁡e=x∈E⟼fx⁡e
20 19 eqeq2d ⊢g=x∈E⟼fx→fe=g⁡e↔fe=x∈E⟼fx⁡e
21 20 ralbidv ⊢g=x∈E⟼fx→∀e∈Efe=g⁡e↔∀e∈Efe=x∈E⟼fx⁡e
22 18 21 anbi12d ⊢g=x∈E⟼fx→g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e↔x∈E⟼fx:E⟶1-1 ontoK∧∀e∈Efe=x∈E⟼fx⁡e
23 22 spcegv ⊢x∈E⟼fx∈V→x∈E⟼fx:E⟶1-1 ontoK∧∀e∈Efe=x∈E⟼fx⁡e→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
24 6 17 23 mpsyl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
25 24 ex ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e