Metamath Proof Explorer

Theorem dfgric2

Description: Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

Ref Expression
Hypotheses dfgric2.v ⊢ V = Vtx ⁡ A
dfgric2.w ⊢ W = Vtx ⁡ B
dfgric2.i ⊢ I = iEdg ⁡ A
dfgric2.j ⊢ J = iEdg ⁡ B
Assertion dfgric2 ⊢ A ∈ X ∧ B ∈ Y → A ≃ 𝑔𝑟 B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i

Proof

Step Hyp Ref Expression
1 dfgric2.v ⊢ V = Vtx ⁡ A
2 dfgric2.w ⊢ W = Vtx ⁡ B
3 dfgric2.i ⊢ I = iEdg ⁡ A
4 dfgric2.j ⊢ J = iEdg ⁡ 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 vex ⊢ f ∈ V
9 1 2 3 4 isgrim ⊢ A ∈ X ∧ B ∈ Y ∧ f ∈ V → f ∈ A GraphIso B ↔ f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I J ⁡ g ⁡ i = f I ⁡ i
10 eqcom ⊢ J ⁡ g ⁡ i = f I ⁡ i ↔ f I ⁡ i = J ⁡ g ⁡ i
11 10 ralbii ⊢ ∀ i ∈ dom ⁡ I J ⁡ g ⁡ i = f I ⁡ i ↔ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
12 11 anbi2i ⊢ g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I J ⁡ g ⁡ i = f I ⁡ i ↔ g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
13 12 exbii ⊢ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I J ⁡ g ⁡ i = f I ⁡ i ↔ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
14 13 anbi2i ⊢ f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I J ⁡ g ⁡ i = f I ⁡ i ↔ f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
15 9 14 bitrdi ⊢ A ∈ X ∧ B ∈ Y ∧ f ∈ V → f ∈ A GraphIso B ↔ f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
16 8 15 mp3an3 ⊢ A ∈ X ∧ B ∈ Y → f ∈ A GraphIso B ↔ f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
17 16 exbidv ⊢ A ∈ X ∧ B ∈ Y → ∃ f f ∈ A GraphIso B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
18 7 17 bitrid ⊢ A ∈ X ∧ B ∈ Y → A ≃ 𝑔𝑟 B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i