Metamath Proof Explorer

Theorem isomuspgr

Description: The isomorphy relation for two simple pseudographs. This corresponds to the definition in Bollobas p. 3. (Contributed by AV, 1-Dec-2022)

Ref Expression
Hypotheses isomushgr.v 
|- V = ( Vtx ` A )
isomushgr.w 
|- W = ( Vtx ` B )
isomushgr.e 
|- E = ( Edg ` A )
isomushgr.k 
|- K = ( Edg ` B )
Assertion isomuspgr 
|- ( ( A e. USPGraph /\ B e. USPGraph ) -> ( A IsomGr B <-> E. f ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )

Proof

Step Hyp Ref Expression
1 isomushgr.v 
 |-  V = ( Vtx ` A )
2 isomushgr.w 
 |-  W = ( Vtx ` B )
3 isomushgr.e 
 |-  E = ( Edg ` A )
4 isomushgr.k 
 |-  K = ( Edg ` B )
5 uspgrushgr 
 |-  ( A e. USPGraph -> A e. USHGraph )
6 uspgrushgr 
 |-  ( B e. USPGraph -> B e. USHGraph )
7 1 2 3 4 isomushgr 
 |-  ( ( A e. USHGraph /\ B e. USHGraph ) -> ( A IsomGr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) ) )
8 5 6 7 syl2an 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( A IsomGr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) ) )
9 imaeq2 
 |-  ( e = { a , b } -> ( f " e ) = ( f " { a , b } ) )
10 fveq2 
 |-  ( e = { a , b } -> ( g ` e ) = ( g ` { a , b } ) )
11 9 10 eqeq12d 
 |-  ( e = { a , b } -> ( ( f " e ) = ( g ` e ) <-> ( f " { a , b } ) = ( g ` { a , b } ) ) )
12 11 rspccv 
 |-  ( A. e e. E ( f " e ) = ( g ` e ) -> ( { a , b } e. E -> ( f " { a , b } ) = ( g ` { a , b } ) ) )
13 12 adantl 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) -> ( { a , b } e. E -> ( f " { a , b } ) = ( g ` { a , b } ) ) )
14 13 imp 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) /\ { a , b } e. E ) -> ( f " { a , b } ) = ( g ` { a , b } ) )
15 f1ofn 
 |-  ( f : V -1-1-onto-> W -> f Fn V )
16 15 ad3antlr 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) -> f Fn V )
17 simprl 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) -> a e. V )
18 simprr 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) -> b e. V )
19 fnimapr 
 |-  ( ( f Fn V /\ a e. V /\ b e. V ) -> ( f " { a , b } ) = { ( f ` a ) , ( f ` b ) } )
20 16 17 18 19 syl3anc 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) -> ( f " { a , b } ) = { ( f ` a ) , ( f ` b ) } )
21 20 eqeq1d 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) -> ( ( f " { a , b } ) = ( g ` { a , b } ) <-> { ( f ` a ) , ( f ` b ) } = ( g ` { a , b } ) ) )
22 21 adantr 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) -> ( ( f " { a , b } ) = ( g ` { a , b } ) <-> { ( f ` a ) , ( f ` b ) } = ( g ` { a , b } ) ) )
23 22 adantr 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) /\ { a , b } e. E ) -> ( ( f " { a , b } ) = ( g ` { a , b } ) <-> { ( f ` a ) , ( f ` b ) } = ( g ` { a , b } ) ) )
24 f1of 
 |-  ( g : E -1-1-onto-> K -> g : E --> K )
25 24 ad3antlr 
 |-  ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) -> g : E --> K )
26 25 ffvelrnda 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) /\ { a , b } e. E ) -> ( g ` { a , b } ) e. K )
27 eleq1 
 |-  ( { ( f ` a ) , ( f ` b ) } = ( g ` { a , b } ) -> ( { ( f ` a ) , ( f ` b ) } e. K <-> ( g ` { a , b } ) e. K ) )
28 26 27 syl5ibrcom 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) /\ { a , b } e. E ) -> ( { ( f ` a ) , ( f ` b ) } = ( g ` { a , b } ) -> { ( f ` a ) , ( f ` b ) } e. K ) )
29 23 28 sylbid 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) /\ { a , b } e. E ) -> ( ( f " { a , b } ) = ( g ` { a , b } ) -> { ( f ` a ) , ( f ` b ) } e. K ) )
30 14 29 mpd 
 |-  ( ( ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) /\ ( a e. V /\ b e. V ) ) /\ A. e e. E ( f " e ) = ( g ` e ) ) /\ { a , b } e. E ) -> { ( f ` a ) , ( f ` b ) } e. K )
31 30 exp41 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) -> ( ( a e. V /\ b e. V ) -> ( A. e e. E ( f " e ) = ( g ` e ) -> ( { a , b } e. E -> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )
32 31 com23 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ g : E -1-1-onto-> K ) -> ( A. e e. E ( f " e ) = ( g ` e ) -> ( ( a e. V /\ b e. V ) -> ( { a , b } e. E -> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )
33 32 impr 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( ( a e. V /\ b e. V ) -> ( { a , b } e. E -> { ( f ` a ) , ( f ` b ) } e. K ) ) )
34 33 imp 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> ( { a , b } e. E -> { ( f ` a ) , ( f ` b ) } e. K ) )
35 1 2 3 4 isomuspgrlem1 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> ( { ( f ` a ) , ( f ` b ) } e. K -> { a , b } e. E ) )
36 34 35 impbid 
 |-  ( ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ ( a e. V /\ b e. V ) ) -> ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) )
37 36 ralrimivva 
 |-  ( ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) )
38 37 ex 
 |-  ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) -> ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) )
39 38 exlimdv 
 |-  ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) -> ( E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) )
40 1 2 3 4 isomuspgrlem2 
 |-  ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) -> ( A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )
41 39 40 impbid 
 |-  ( ( ( A e. USPGraph /\ B e. USPGraph ) /\ f : V -1-1-onto-> W ) -> ( E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) <-> A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) )
42 41 pm5.32da 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) <-> ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )
43 42 exbidv 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( E. f ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) <-> E. f ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )
44 8 43 bitrd 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( A IsomGr B <-> E. f ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )