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 ⟼ F x
isomuspgrlem2.a ⊢ φ → A ∈ USHGraph
isomuspgrlem2.f ⊢ φ → F : V ⟶ 1-1 onto W
isomuspgrlem2.i ⊢ φ → ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ F ⁡ a F ⁡ b ∈ K
isomuspgrlem2.x ⊢ φ → F ∈ X
Assertion isomuspgrlem2c ⊢ φ → G : E ⟶ 1-1 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 ⟼ F x
6 isomuspgrlem2.a ⊢ φ → A ∈ USHGraph
7 isomuspgrlem2.f ⊢ φ → F : V ⟶ 1-1 onto W
8 isomuspgrlem2.i ⊢ φ → ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ F ⁡ a F ⁡ 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 ∈ E F e = G ⁡ e
12 9 11 syl ⊢ φ → ∀ e ∈ E F e = G ⁡ e
13 imaeq2 ⊢ e = c → F e = F c
14 fveq2 ⊢ e = c → G ⁡ e = G ⁡ c
15 13 14 eqeq12d ⊢ e = c → F e = G ⁡ e ↔ F c = G ⁡ c
16 15 rspcv ⊢ c ∈ E → ∀ e ∈ E F e = G ⁡ e → F c = G ⁡ c
17 16 ad2antrl ⊢ φ ∧ c ∈ E ∧ d ∈ E → ∀ e ∈ E F e = G ⁡ e → F c = G ⁡ c
18 17 imp ⊢ φ ∧ c ∈ E ∧ d ∈ E ∧ ∀ e ∈ E F e = G ⁡ e → F c = G ⁡ c
19 18 eqcomd ⊢ φ ∧ c ∈ E ∧ d ∈ E ∧ ∀ e ∈ E F e = G ⁡ e → G ⁡ c = F c
20 imaeq2 ⊢ e = d → F e = F d
21 fveq2 ⊢ e = d → G ⁡ e = G ⁡ d
22 20 21 eqeq12d ⊢ e = d → F e = G ⁡ e ↔ F d = G ⁡ d
23 22 rspcv ⊢ d ∈ E → ∀ e ∈ E F e = G ⁡ e → F d = G ⁡ d
24 23 ad2antll ⊢ φ ∧ c ∈ E ∧ d ∈ E → ∀ e ∈ E F e = G ⁡ e → F d = G ⁡ d
25 24 imp ⊢ φ ∧ c ∈ E ∧ d ∈ E ∧ ∀ e ∈ E F e = G ⁡ e → F d = G ⁡ d
26 25 eqcomd ⊢ φ ∧ c ∈ E ∧ d ∈ E ∧ ∀ e ∈ E F e = G ⁡ e → G ⁡ d = F d
27 19 26 eqeq12d ⊢ φ ∧ c ∈ E ∧ d ∈ E ∧ ∀ e ∈ E F e = G ⁡ e → G ⁡ c = G ⁡ d ↔ F c = F d
28 12 27 mpidan ⊢ φ ∧ c ∈ E ∧ d ∈ E → G ⁡ c = G ⁡ d ↔ F c = F d
29 f1of1 ⊢ F : V ⟶ 1-1 onto W → F : V ⟶ 1-1 W
30 7 29 syl ⊢ φ → F : V ⟶ 1-1 W
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 syl5bi ⊢ 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 syl5bi ⊢ 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-1 W ∧ c ⊆ V ∧ d ⊆ V → F c = F d ↔ c = d
52 30 50 51 syl2an2r ⊢ φ ∧ c ∈ E ∧ d ∈ E → F c = F d ↔ c = d
53 52 biimpd ⊢ φ ∧ c ∈ E ∧ d ∈ E → F c = F d → c = d
54 28 53 sylbid ⊢ φ ∧ c ∈ E ∧ d ∈ E → G ⁡ c = G ⁡ d → c = d
55 54 ralrimivva ⊢ φ → ∀ c ∈ E ∀ d ∈ E G ⁡ c = G ⁡ d → c = d
56 dff13 ⊢ G : E ⟶ 1-1 K ↔ G : E ⟶ K ∧ ∀ c ∈ E ∀ d ∈ E G ⁡ c = G ⁡ d → c = d
57 10 55 56 sylanbrc ⊢ φ → G : E ⟶ 1-1 K