Metamath Proof Explorer

Theorem isomuspgrlem2c

Description: Lemma 3 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
isomuspgrlem2.x ⊢φ→F∈X
Assertion isomuspgrlem2c ⊢φ→G:E⟶1-1K

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 1 2 3 4 5 6 7 8 isomuspgrlem2b ⊢φ→G:E⟶K
11 1 2 3 4 5 isomuspgrlem2a ⊢F∈X→∀e∈EFe=G⁡e
12 9 11 syl ⊢φ→∀e∈EFe=G⁡e
13 imaeq2 ⊢e=c→Fe=Fc
14 fveq2 ⊢e=c→G⁡e=G⁡c
15 13 14 eqeq12d ⊢e=c→Fe=G⁡e↔Fc=G⁡c
16 15 rspcv ⊢c∈E→∀e∈EFe=G⁡e→Fc=G⁡c
17 16 ad2antrl ⊢φ∧c∈E∧d∈E→∀e∈EFe=G⁡e→Fc=G⁡c
18 17 imp ⊢φ∧c∈E∧d∈E∧∀e∈EFe=G⁡e→Fc=G⁡c
19 18 eqcomd ⊢φ∧c∈E∧d∈E∧∀e∈EFe=G⁡e→G⁡c=Fc
20 imaeq2 ⊢e=d→Fe=Fd
21 fveq2 ⊢e=d→G⁡e=G⁡d
22 20 21 eqeq12d ⊢e=d→Fe=G⁡e↔Fd=G⁡d
23 22 rspcv ⊢d∈E→∀e∈EFe=G⁡e→Fd=G⁡d
24 23 ad2antll ⊢φ∧c∈E∧d∈E→∀e∈EFe=G⁡e→Fd=G⁡d
25 24 imp ⊢φ∧c∈E∧d∈E∧∀e∈EFe=G⁡e→Fd=G⁡d
26 25 eqcomd ⊢φ∧c∈E∧d∈E∧∀e∈EFe=G⁡e→G⁡d=Fd
27 19 26 eqeq12d ⊢φ∧c∈E∧d∈E∧∀e∈EFe=G⁡e→G⁡c=G⁡d↔Fc=Fd
28 12 27 mpidan ⊢φ∧c∈E∧d∈E→G⁡c=G⁡d↔Fc=Fd
29 f1of1 ⊢F:V⟶1-1 ontoW→F:V⟶1-1W
30 7 29 syl ⊢φ→F:V⟶1-1W
31 uspgrupgr ⊢A∈USHGraph→A∈UPGraph
32 upgruhgr ⊢A∈UPGraph→A∈UHGraph
33 3 eleq2i ⊢c∈E↔c∈Edg⁡A
34 edguhgr ⊢A∈UHGraph∧c∈Edg⁡A→c∈𝒫Vtx⁡A
35 elpwi ⊢c∈𝒫Vtx⁡A→c⊆Vtx⁡A
36 35 1 sseqtrrdi ⊢c∈𝒫Vtx⁡A→c⊆V
37 34 36 syl ⊢A∈UHGraph∧c∈Edg⁡A→c⊆V
38 37 ex ⊢A∈UHGraph→c∈Edg⁡A→c⊆V
39 33 38 biimtrid ⊢A∈UHGraph→c∈E→c⊆V
40 3 eleq2i ⊢d∈E↔d∈Edg⁡A
41 edguhgr ⊢A∈UHGraph∧d∈Edg⁡A→d∈𝒫Vtx⁡A
42 elpwi ⊢d∈𝒫Vtx⁡A→d⊆Vtx⁡A
43 42 1 sseqtrrdi ⊢d∈𝒫Vtx⁡A→d⊆V
44 41 43 syl ⊢A∈UHGraph∧d∈Edg⁡A→d⊆V
45 44 ex ⊢A∈UHGraph→d∈Edg⁡A→d⊆V
46 40 45 biimtrid ⊢A∈UHGraph→d∈E→d⊆V
47 39 46 anim12d ⊢A∈UHGraph→c∈E∧d∈E→c⊆V∧d⊆V
48 32 47 syl ⊢A∈UPGraph→c∈E∧d∈E→c⊆V∧d⊆V
49 6 31 48 3syl ⊢φ→c∈E∧d∈E→c⊆V∧d⊆V
50 49 imp ⊢φ∧c∈E∧d∈E→c⊆V∧d⊆V
51 f1imaeq ⊢F:V⟶1-1W∧c⊆V∧d⊆V→Fc=Fd↔c=d
52 30 50 51 syl2an2r ⊢φ∧c∈E∧d∈E→Fc=Fd↔c=d
53 52 biimpd ⊢φ∧c∈E∧d∈E→Fc=Fd→c=d
54 28 53 sylbid ⊢φ∧c∈E∧d∈E→G⁡c=G⁡d→c=d
55 54 ralrimivva ⊢φ→∀c∈E∀d∈EG⁡c=G⁡d→c=d
56 dff13 ⊢G:E⟶1-1K↔G:E⟶K∧∀c∈E∀d∈EG⁡c=G⁡d→c=d
57 10 55 56 sylanbrc ⊢φ→G:E⟶1-1K