Metamath Proof Explorer

Theorem uspgrbisymrelALT

Description: Alternate proof of uspgrbisymrel not using the definition of equinumerosity. (Contributed by AV, 26-Nov-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses uspgrbisymrel.g 
|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
uspgrbisymrel.r 
|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
Assertion uspgrbisymrelALT 
|- ( V e. W -> E. f f : G -1-1-onto-> R )

Proof

Step Hyp Ref Expression
1 uspgrbisymrel.g 
 |-  G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
2 uspgrbisymrel.r 
 |-  R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
3 fvex 
 |-  ( Pairs ` V ) e. _V
4 3 pwex 
 |-  ~P ( Pairs ` V ) e. _V
5 mptexg 
 |-  ( ~P ( Pairs ` V ) e. _V -> ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) e. _V )
6 4 5 mp1i 
 |-  ( V e. W -> ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) e. _V )
7 eqid 
 |-  ~P ( Pairs ` V ) = ~P ( Pairs ` V )
8 7 1 uspgrex 
 |-  ( V e. W -> G e. _V )
9 mptexg 
 |-  ( G e. _V -> ( g e. G |-> ( 2nd ` g ) ) e. _V )
10 8 9 syl 
 |-  ( V e. W -> ( g e. G |-> ( 2nd ` g ) ) e. _V )
11 coexg 
 |-  ( ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) e. _V /\ ( g e. G |-> ( 2nd ` g ) ) e. _V ) -> ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) e. _V )
12 6 10 11 syl2anc 
 |-  ( V e. W -> ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) e. _V )
13 eqid 
 |-  ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) = ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } )
14 7 2 13 sprsymrelf1o 
 |-  ( V e. W -> ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) : ~P ( Pairs ` V ) -1-1-onto-> R )
15 eqid 
 |-  ( g e. G |-> ( 2nd ` g ) ) = ( g e. G |-> ( 2nd ` g ) )
16 7 1 15 uspgrsprf1o 
 |-  ( V e. W -> ( g e. G |-> ( 2nd ` g ) ) : G -1-1-onto-> ~P ( Pairs ` V ) )
17 f1oco 
 |-  ( ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) : ~P ( Pairs ` V ) -1-1-onto-> R /\ ( g e. G |-> ( 2nd ` g ) ) : G -1-1-onto-> ~P ( Pairs ` V ) ) -> ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) : G -1-1-onto-> R )
18 14 16 17 syl2anc 
 |-  ( V e. W -> ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) : G -1-1-onto-> R )
19 f1oeq1 
 |-  ( f = ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) -> ( f : G -1-1-onto-> R <-> ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) : G -1-1-onto-> R ) )
20 19 spcegv 
 |-  ( ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) e. _V -> ( ( ( p e. ~P ( Pairs ` V ) |-> { <. x , y >. | E. c e. p c = { x , y } } ) o. ( g e. G |-> ( 2nd ` g ) ) ) : G -1-1-onto-> R -> E. f f : G -1-1-onto-> R ) )
21 12 18 20 sylc 
 |-  ( V e. W -> E. f f : G -1-1-onto-> R )