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 
|- 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 ) ) )