Metamath Proof Explorer

Theorem gricuspgr

Description: The "is isomorphic to" relation for two simple pseudographs. This corresponds to the definition in Bollobas p. 3. (Contributed by AV, 1-Dec-2022) (Proof shortened by AV, 5-May-2025)

Ref Expression
Hypotheses gricushgr.v ⊢ V = Vtx ⁡ A
gricushgr.w ⊢ W = Vtx ⁡ B
gricushgr.e ⊢ E = Edg ⁡ A
gricushgr.k ⊢ K = Edg ⁡ B
Assertion gricuspgr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A ≃ 𝑔𝑟 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 gricushgr.v ⊢ V = Vtx ⁡ A
2 gricushgr.w ⊢ W = Vtx ⁡ B
3 gricushgr.e ⊢ E = Edg ⁡ A
4 gricushgr.k ⊢ K = Edg ⁡ B
5 brgric ⊢ A ≃ 𝑔𝑟 B ↔ A GraphIso B ≠ ∅
6 n0 ⊢ A GraphIso B ≠ ∅ ↔ ∃ f f ∈ A GraphIso B
7 5 6 bitri ⊢ A ≃ 𝑔𝑟 B ↔ ∃ f f ∈ A GraphIso B
8 7 a1i ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A ≃ 𝑔𝑟 B ↔ ∃ f f ∈ A GraphIso B
9 1 2 3 4 isuspgrim ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → f ∈ A GraphIso B ↔ f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
10 9 exbidv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → ∃ f f ∈ A GraphIso B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K
11 8 10 bitrd ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A ≃ 𝑔𝑟 B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ a ∈ V ∀ b ∈ V a b ∈ E ↔ f ⁡ a f ⁡ b ∈ K