Metamath Proof Explorer

Theorem isomgr

Description: The isomorphy relation for two graphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Hypotheses isomgr.v ⊢ V = Vtx ⁡ A
isomgr.w ⊢ W = Vtx ⁡ B
isomgr.i ⊢ I = iEdg ⁡ A
isomgr.j ⊢ J = iEdg ⁡ B
Assertion isomgr ⊢ A ∈ X ∧ B ∈ Y → A IsomGr 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 isomgr.v ⊢ V = Vtx ⁡ A
2 isomgr.w ⊢ W = Vtx ⁡ B
3 isomgr.i ⊢ I = iEdg ⁡ A
4 isomgr.j ⊢ J = iEdg ⁡ B
5 eqidd ⊢ x = A ∧ y = B → f = f
6 fveq2 ⊢ x = A → Vtx ⁡ x = Vtx ⁡ A
7 6 adantr ⊢ x = A ∧ y = B → Vtx ⁡ x = Vtx ⁡ A
8 7 1 eqtr4di ⊢ x = A ∧ y = B → Vtx ⁡ x = V
9 fveq2 ⊢ y = B → Vtx ⁡ y = Vtx ⁡ B
10 9 adantl ⊢ x = A ∧ y = B → Vtx ⁡ y = Vtx ⁡ B
11 10 2 eqtr4di ⊢ x = A ∧ y = B → Vtx ⁡ y = W
12 5 8 11 f1oeq123d ⊢ x = A ∧ y = B → f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ↔ f : V ⟶ 1-1 onto W
13 eqidd ⊢ x = A ∧ y = B → g = g
14 fveq2 ⊢ x = A → iEdg ⁡ x = iEdg ⁡ A
15 14 adantr ⊢ x = A ∧ y = B → iEdg ⁡ x = iEdg ⁡ A
16 15 3 eqtr4di ⊢ x = A ∧ y = B → iEdg ⁡ x = I
17 16 dmeqd ⊢ x = A ∧ y = B → dom ⁡ iEdg ⁡ x = dom ⁡ I
18 fveq2 ⊢ y = B → iEdg ⁡ y = iEdg ⁡ B
19 18 adantl ⊢ x = A ∧ y = B → iEdg ⁡ y = iEdg ⁡ B
20 19 4 eqtr4di ⊢ x = A ∧ y = B → iEdg ⁡ y = J
21 20 dmeqd ⊢ x = A ∧ y = B → dom ⁡ iEdg ⁡ y = dom ⁡ J
22 13 17 21 f1oeq123d ⊢ x = A ∧ y = B → g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ↔ g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J
23 16 fveq1d ⊢ x = A ∧ y = B → iEdg ⁡ x ⁡ i = I ⁡ i
24 23 imaeq2d ⊢ x = A ∧ y = B → f iEdg ⁡ x ⁡ i = f I ⁡ i
25 20 fveq1d ⊢ x = A ∧ y = B → iEdg ⁡ y ⁡ g ⁡ i = J ⁡ g ⁡ i
26 24 25 eqeq12d ⊢ x = A ∧ y = B → f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i ↔ f I ⁡ i = J ⁡ g ⁡ i
27 17 26 raleqbidv ⊢ x = A ∧ y = B → ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i ↔ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
28 22 27 anbi12d ⊢ x = A ∧ y = B → g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i ↔ g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
29 28 exbidv ⊢ x = A ∧ y = B → ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i ↔ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
30 12 29 anbi12d ⊢ x = A ∧ y = B → f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ 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
31 30 exbidv ⊢ x = A ∧ y = B → ∃ f f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i ↔ ∃ 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
32 df-isomgr ⊢ IsomGr = x y | ∃ f f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
33 31 32 brabga ⊢ A ∈ X ∧ B ∈ Y → A IsomGr 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