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→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) )