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 ‘ 𝐺 ) ) → ( 𝐾 ∈ 𝐸 ↔ ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )