Metamath Proof Explorer

Theorem isomuspgr

Description: The isomorphy relation for two simple pseudographs. This corresponds to the definition in Bollobas p. 3. (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 isomuspgr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ 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 uspgrushgr ⊢ A ∈ USHGraph → A ∈ USHGraph
6 uspgrushgr ⊢ B ∈ USHGraph → B ∈ USHGraph
7 1 2 3 4 isomushgr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
8 5 6 7 syl2an ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
9 imaeq2 ⊢ e = a b → f e = f a b
10 fveq2 ⊢ e = a b → g ⁡ e = g ⁡ a b
11 9 10 eqeq12d ⊢ e = a b → f e = g ⁡ e ↔ f a b = g ⁡ a b
12 11 rspccv ⊢ ∀ e ∈ E f e = g ⁡ e → a b ∈ E → f a b = g ⁡ a b
13 12 adantl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e → a b ∈ E → f a b = g ⁡ a b
14 13 imp ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e ∧ a b ∈ E → f a b = g ⁡ a b
15 f1ofn ⊢ f : V ⟶ 1-1 onto W → f Fn V
16 15 ad3antlr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V → f Fn V
17 simprl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V → a ∈ V
18 simprr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V → b ∈ V
19 fnimapr ⊢ f Fn V ∧ a ∈ V ∧ b ∈ V → f a b = f ⁡ a f ⁡ b
20 16 17 18 19 syl3anc ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V → f a b = f ⁡ a f ⁡ b
21 20 eqeq1d ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V → f a b = g ⁡ a b ↔ f ⁡ a f ⁡ b = g ⁡ a b
22 21 adantr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e → f a b = g ⁡ a b ↔ f ⁡ a f ⁡ b = g ⁡ a b
23 22 adantr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e ∧ a b ∈ E → f a b = g ⁡ a b ↔ f ⁡ a f ⁡ b = g ⁡ a b
24 f1of ⊢ g : E ⟶ 1-1 onto K → g : E ⟶ K
25 24 ad3antlr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e → g : E ⟶ K
26 25 ffvelrnda ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e ∧ a b ∈ E → g ⁡ a b ∈ K
27 eleq1 ⊢ f ⁡ a f ⁡ b = g ⁡ a b → f ⁡ a f ⁡ b ∈ K ↔ g ⁡ a b ∈ K
28 26 27 syl5ibrcom ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e ∧ a b ∈ E → f ⁡ a f ⁡ b = g ⁡ a b → f ⁡ a f ⁡ b ∈ K
29 23 28 sylbid ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e ∧ a b ∈ E → f a b = g ⁡ a b → f ⁡ a f ⁡ b ∈ K
30 14 29 mpd ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ a ∈ V ∧ b ∈ V ∧ ∀ e ∈ E f e = g ⁡ e ∧ a b ∈ E → f ⁡ a f ⁡ b ∈ K
31 30 exp41 ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K → a ∈ V ∧ b ∈ V → ∀ e ∈ E f e = g ⁡ e → a b ∈ E → f ⁡ a f ⁡ b ∈ K
32 31 com23 ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K → ∀ e ∈ E f e = g ⁡ e → a ∈ V ∧ b ∈ V → a b ∈ E → f ⁡ a f ⁡ b ∈ K
33 32 impr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → a ∈ V ∧ b ∈ V → a b ∈ E → f ⁡ a f ⁡ b ∈ K
34 33 imp ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ a ∈ V ∧ b ∈ V → a b ∈ E → f ⁡ a f ⁡ b ∈ K
35 1 2 3 4 isomuspgrlem1 ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ a ∈ V ∧ b ∈ V → f ⁡ a f ⁡ b ∈ K → a b ∈ E
36 34 35 impbid ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ a ∈ V ∧ b ∈ V → a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
37 36 ralrimivva ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
38 37 ex ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
39 38 exlimdv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
40 1 2 3 4 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
41 39 40 impbid ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ↔ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
42 41 pm5.32da ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ↔ f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
43 42 exbidv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
44 8 43 bitrd ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K