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