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	|- E = ( Edg ` G )
	uhgrimedgi.d	|- D = ( Edg ` H )
	uhgrimprop.v	|- V = ( Vtx ` G )
	uhgrimprop.w	|- W = ( Vtx ` H )
Assertion	uhgrimprop	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) )

Proof

Step	Hyp	Ref	Expression
1		uhgrimedgi.e	|- E = ( Edg ` G )
2		uhgrimedgi.d	|- D = ( Edg ` H )
3		uhgrimprop.v	|- V = ( Vtx ` G )
4		uhgrimprop.w	|- W = ( Vtx ` H )
5	3 4	grimf1o	|- ( F e. ( G GraphIso H ) -> F : V -1-1-onto-> W )
6	5	3ad2ant3	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> F : V -1-1-onto-> W )
7		3simpa	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( G e. UHGraph /\ H e. UHGraph ) )
8		simp3	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> F e. ( G GraphIso H ) )
9		prssi	|- ( ( x e. V /\ y e. V ) -> { x , y } C_ V )
10	9 3	sseqtrdi	|- ( ( x e. V /\ y e. V ) -> { x , y } C_ ( Vtx ` G ) )
11	1 2	uhgrimedg	|- ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ { x , y } C_ ( Vtx ` G ) ) -> ( { x , y } e. E <-> ( F " { x , y } ) e. D ) )
12	7 8 10 11	syl2an3an	|- ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E <-> ( F " { x , y } ) e. D ) )
13		f1ofn	|- ( F : V -1-1-onto-> W -> F Fn V )
14	5 13	syl	|- ( F e. ( G GraphIso H ) -> F Fn V )
15	14	3ad2ant3	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> F Fn V )
16	15	anim1i	|- ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ ( x e. V /\ y e. V ) ) -> ( F Fn V /\ ( x e. V /\ y e. V ) ) )
17		3anass	|- ( ( F Fn V /\ x e. V /\ y e. V ) <-> ( F Fn V /\ ( x e. V /\ y e. V ) ) )
18	16 17	sylibr	|- ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ ( x e. V /\ y e. V ) ) -> ( F Fn V /\ x e. V /\ y e. V ) )
19		fnimapr	|- ( ( F Fn V /\ x e. V /\ y e. V ) -> ( F " { x , y } ) = { ( F ` x ) , ( F ` y ) } )
20	18 19	syl	|- ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ ( x e. V /\ y e. V ) ) -> ( F " { x , y } ) = { ( F ` x ) , ( F ` y ) } )
21	20	eleq1d	|- ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ ( x e. V /\ y e. V ) ) -> ( ( F " { x , y } ) e. D <-> { ( F ` x ) , ( F ` y ) } e. D ) )
22	12 21	bitrd	|- ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) )
23	22	ralrimivva	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) )
24	6 23	jca	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) )