Metamath Proof Explorer

Theorem grimprop

Description: Properties of an isomorphism of graphs. (Contributed by AV, 29-Apr-2025)

Ref Expression
Hypotheses grimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
grimprop.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
grimprop.d ⊢ 𝐷 = ( iEdg ‘ 𝐻 )
Assertion grimprop ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 grimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 grimprop.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4 grimprop.d ⊢ 𝐷 = ( iEdg ‘ 𝐻 )
5 grimdmrel ⊢ Rel dom GraphIso
6 5 ovrcl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
7 6 simpld ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐺 ∈ V )
8 6 simprd ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐻 ∈ V )
9 id ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
10 7 8 9 3jca ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
11 1 2 3 4 isgrim ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
12 11 biimpd ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
13 10 12 mpcom ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) )