Metamath Proof Explorer

Theorem isgrim

Description: An isomorphism of graphs is a bijection between their vertices that preserves adjacency. (Contributed by AV, 19-Apr-2025)

Ref Expression
Hypotheses isgrim.v ⊢ V = Vtx ⁡ G
isgrim.w ⊢ W = Vtx ⁡ H
isgrim.e ⊢ E = iEdg ⁡ G
isgrim.d ⊢ D = iEdg ⁡ H
Assertion isgrim ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphIso H ↔ F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i

Proof

Step Hyp Ref Expression
1 isgrim.v ⊢ V = Vtx ⁡ G
2 isgrim.w ⊢ W = Vtx ⁡ H
3 isgrim.e ⊢ E = iEdg ⁡ G
4 isgrim.d ⊢ D = iEdg ⁡ H
5 df-grim ⊢ GraphIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
6 elex ⊢ G ∈ X → G ∈ V
7 6 3ad2ant1 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → G ∈ V
8 elex ⊢ H ∈ Y → H ∈ V
9 8 3ad2ant2 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → H ∈ V
10 f1of ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → f : Vtx ⁡ G ⟶ Vtx ⁡ H
11 fvex ⊢ Vtx ⁡ H ∈ V
12 fvex ⊢ Vtx ⁡ G ∈ V
13 11 12 elmap ⊢ f ∈ Vtx ⁡ H Vtx ⁡ G ↔ f : Vtx ⁡ G ⟶ Vtx ⁡ H
14 10 13 sylibr ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → f ∈ Vtx ⁡ H Vtx ⁡ G
15 14 adantr ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i → f ∈ Vtx ⁡ H Vtx ⁡ G
16 ovex ⊢ Vtx ⁡ H Vtx ⁡ G ∈ V
17 15 16 abex ⊢ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ∈ V
18 17 a1i ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ∈ V
19 eqidd ⊢ g = G ∧ h = H → f = f
20 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
21 20 adantr ⊢ g = G ∧ h = H → Vtx ⁡ g = Vtx ⁡ G
22 fveq2 ⊢ h = H → Vtx ⁡ h = Vtx ⁡ H
23 22 adantl ⊢ g = G ∧ h = H → Vtx ⁡ h = Vtx ⁡ H
24 19 21 23 f1oeq123d ⊢ g = G ∧ h = H → f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ↔ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
25 fvexd ⊢ g = G ∧ h = H → iEdg ⁡ g ∈ V
26 fveq2 ⊢ g = G → iEdg ⁡ g = iEdg ⁡ G
27 26 adantr ⊢ g = G ∧ h = H → iEdg ⁡ g = iEdg ⁡ G
28 fvexd ⊢ g = G ∧ h = H ∧ e = iEdg ⁡ G → iEdg ⁡ h ∈ V
29 fveq2 ⊢ h = H → iEdg ⁡ h = iEdg ⁡ H
30 29 adantl ⊢ g = G ∧ h = H → iEdg ⁡ h = iEdg ⁡ H
31 30 adantr ⊢ g = G ∧ h = H ∧ e = iEdg ⁡ G → iEdg ⁡ h = iEdg ⁡ H
32 eqidd ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → j = j
33 dmeq ⊢ e = iEdg ⁡ G → dom ⁡ e = dom ⁡ iEdg ⁡ G
34 33 adantr ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → dom ⁡ e = dom ⁡ iEdg ⁡ G
35 dmeq ⊢ d = iEdg ⁡ H → dom ⁡ d = dom ⁡ iEdg ⁡ H
36 35 adantl ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → dom ⁡ d = dom ⁡ iEdg ⁡ H
37 32 34 36 f1oeq123d ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H
38 fveq1 ⊢ d = iEdg ⁡ H → d ⁡ j ⁡ i = iEdg ⁡ H ⁡ j ⁡ i
39 fveq1 ⊢ e = iEdg ⁡ G → e ⁡ i = iEdg ⁡ G ⁡ i
40 39 imaeq2d ⊢ e = iEdg ⁡ G → f e ⁡ i = f iEdg ⁡ G ⁡ i
41 38 40 eqeqan12rd ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → d ⁡ j ⁡ i = f e ⁡ i ↔ iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
42 34 41 raleqbidv ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
43 37 42 anbi12d ⊢ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
44 43 adantll ⊢ g = G ∧ h = H ∧ e = iEdg ⁡ G ∧ d = iEdg ⁡ H → j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
45 28 31 44 sbcied2 ⊢ g = G ∧ h = H ∧ e = iEdg ⁡ G → [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
46 25 27 45 sbcied2 ⊢ g = G ∧ h = H → [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
47 biidd ⊢ g = G ∧ h = H → j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
48 46 47 bitrd ⊢ g = G ∧ h = H → [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
49 48 exbidv ⊢ g = G ∧ h = H → ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
50 24 49 anbi12d ⊢ g = G ∧ h = H → f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ↔ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
51 50 abbidv ⊢ g = G ∧ h = H → f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i = f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
52 5 7 9 18 51 elovmpod ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphIso H ↔ F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i
53 id ⊢ f = F → f = F
54 1 eqcomi ⊢ Vtx ⁡ G = V
55 54 a1i ⊢ f = F → Vtx ⁡ G = V
56 2 eqcomi ⊢ Vtx ⁡ H = W
57 56 a1i ⊢ f = F → Vtx ⁡ H = W
58 53 55 57 f1oeq123d ⊢ f = F → f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ↔ F : V ⟶ 1-1 onto W
59 eqidd ⊢ f = F → j = j
60 3 eqcomi ⊢ iEdg ⁡ G = E
61 60 dmeqi ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ E
62 61 a1i ⊢ f = F → dom ⁡ iEdg ⁡ G = dom ⁡ E
63 4 eqcomi ⊢ iEdg ⁡ H = D
64 63 dmeqi ⊢ dom ⁡ iEdg ⁡ H = dom ⁡ D
65 64 a1i ⊢ f = F → dom ⁡ iEdg ⁡ H = dom ⁡ D
66 59 62 65 f1oeq123d ⊢ f = F → j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ↔ j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D
67 63 fveq1i ⊢ iEdg ⁡ H ⁡ j ⁡ i = D ⁡ j ⁡ i
68 67 a1i ⊢ f = F → iEdg ⁡ H ⁡ j ⁡ i = D ⁡ j ⁡ i
69 60 fveq1i ⊢ iEdg ⁡ G ⁡ i = E ⁡ i
70 69 a1i ⊢ f = F → iEdg ⁡ G ⁡ i = E ⁡ i
71 53 70 imaeq12d ⊢ f = F → f iEdg ⁡ G ⁡ i = F E ⁡ i
72 68 71 eqeq12d ⊢ f = F → iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ D ⁡ j ⁡ i = F E ⁡ i
73 62 72 raleqbidv ⊢ f = F → ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
74 66 73 anbi12d ⊢ f = F → j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
75 74 exbidv ⊢ f = F → ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
76 58 75 anbi12d ⊢ f = F → f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
77 76 elabg ⊢ F ∈ Z → F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
78 77 3ad2ant3 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = f iEdg ⁡ G ⁡ i ↔ F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
79 52 78 bitrd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphIso H ↔ F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i