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