This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgrimedg

Description: An isomorphism between graphs preserves edges, i.e. there is an edge in one graph connecting vertices iff there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025)

Ref Expression
Hypotheses uhgrimedgi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
uhgrimedgi.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
Assertion uhgrimedg ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐾 ∈ 𝐸 ↔ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 uhgrimedgi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 uhgrimedgi.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
3 simp1 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
4 simp2 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
5 4 anim1i ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ 𝐾 ∈ 𝐸 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ∈ 𝐸 ) )
6 1 2 uhgrimedgi ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ∈ 𝐸 ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 )
7 3 5 6 syl2an2r ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ 𝐾 ∈ 𝐸 ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 )
8 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
10 8 9 grimf1o ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
11 f1of1 ⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
12 10 11 syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
13 12 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
14 simp3 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → 𝐾 ⊆ ( Vtx ‘ 𝐺 ) )
15 13 14 jca ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) )
16 15 adantr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) )
17 f1imacnv ⊢ ( ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐾 ) ) = 𝐾 )
18 16 17 syl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐾 ) ) = 𝐾 )
19 pm3.22 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) )
20 19 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) )
21 simpl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → 𝐺 ∈ UHGraph )
22 21 anim1i ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
23 22 3adant3 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
24 grimcnv ⊢ ( 𝐺 ∈ UHGraph → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ◡ 𝐹 ∈ ( 𝐻 GraphIso 𝐺 ) ) )
25 24 imp ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ◡ 𝐹 ∈ ( 𝐻 GraphIso 𝐺 ) )
26 23 25 syl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ◡ 𝐹 ∈ ( 𝐻 GraphIso 𝐺 ) )
27 26 anim1i ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) → ( ◡ 𝐹 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )
28 2 1 uhgrimedgi ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ ( ◡ 𝐹 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐾 ) ) ∈ 𝐸 )
29 20 27 28 syl2an2r ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐾 ) ) ∈ 𝐸 )
30 18 29 eqeltrrd ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) → 𝐾 ∈ 𝐸 )
31 7 30 impbida ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐾 ∈ 𝐸 ↔ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )