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

Metamath Proof Explorer

Theorem uhgrimprop

Description: An isomorphism between hypergraphs is a bijection between their vertices that preserves adjacency for simple edges, i.e. there is a simple edge in one graph connecting one or two vertices iff there is a simple edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025) (Revised by AV, 25-Oct-2025)

Ref Expression
Hypotheses uhgrimedgi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
uhgrimedgi.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
uhgrimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion uhgrimprop ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 uhgrimedgi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 uhgrimedgi.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
3 uhgrimprop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4 uhgrimprop.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
5 3 4 grimf1o ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
6 5 3ad2ant3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
7 3simpa ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
8 simp3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
9 prssi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → { 𝑥 , 𝑦 } ⊆ 𝑉 )
10 9 3 sseqtrdi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → { 𝑥 , 𝑦 } ⊆ ( Vtx ‘ 𝐺 ) )
11 1 2 uhgrimedg ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ { 𝑥 , 𝑦 } ⊆ ( Vtx ‘ 𝐺 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) )
12 7 8 10 11 syl2an3an ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) )
13 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 Fn 𝑉 )
14 5 13 syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 Fn 𝑉 )
15 14 3ad2ant3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 Fn 𝑉 )
16 15 anim1i ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
17 3anass ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ↔ ( 𝐹 Fn 𝑉 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
18 16 17 sylibr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
19 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) = { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } )
20 18 19 syl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) = { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } )
21 20 eleq1d ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) )
22 12 21 bitrd ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) )
23 22 ralrimivva ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) )
24 6 23 jca ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) )