Metamath Proof Explorer

Theorem sprsymrelfo

Description: The mapping F is a function from the subsets of the set of pairs over a fixed set V onto the symmetric relations R on the fixed set V . (Contributed by AV, 23-Nov-2021)

Ref Expression
Hypotheses sprsymrelf.p 
|- P = ~P ( Pairs ` V )
sprsymrelf.r 
|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
sprsymrelf.f 
|- F = ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } )
Assertion sprsymrelfo 
|- ( V e. W -> F : P -onto-> R )

Proof

Step Hyp Ref Expression
1 sprsymrelf.p 
 |-  P = ~P ( Pairs ` V )
2 sprsymrelf.r 
 |-  R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
3 sprsymrelf.f 
 |-  F = ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } )
4 1 2 3 sprsymrelf 
 |-  F : P --> R
5 4 a1i 
 |-  ( V e. W -> F : P --> R )
6 breq 
 |-  ( r = t -> ( x r y <-> x t y ) )
7 breq 
 |-  ( r = t -> ( y r x <-> y t x ) )
8 6 7 bibi12d 
 |-  ( r = t -> ( ( x r y <-> y r x ) <-> ( x t y <-> y t x ) ) )
9 8 2ralbidv 
 |-  ( r = t -> ( A. x e. V A. y e. V ( x r y <-> y r x ) <-> A. x e. V A. y e. V ( x t y <-> y t x ) ) )
10 9 2 elrab2 
 |-  ( t e. R <-> ( t e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) )
11 eqid 
 |-  { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) }
12 11 sprsymrelfolem1 
 |-  { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } e. ~P ( Pairs ` V )
13 12 1 eleqtrri 
 |-  { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } e. P
14 13 a1i 
 |-  ( ( ( t e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) /\ V e. W ) -> { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } e. P )
15 rexeq 
 |-  ( f = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } -> ( E. c e. f c = { x , y } <-> E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } ) )
16 15 opabbidv 
 |-  ( f = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } -> { <. x , y >. | E. c e. f c = { x , y } } = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } )
17 16 eqeq2d 
 |-  ( f = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } -> ( t = { <. x , y >. | E. c e. f c = { x , y } } <-> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) )
18 17 adantl 
 |-  ( ( ( ( t e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) /\ V e. W ) /\ f = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } ) -> ( t = { <. x , y >. | E. c e. f c = { x , y } } <-> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) )
19 velpw 
 |-  ( t e. ~P ( V X. V ) <-> t C_ ( V X. V ) )
20 xpss 
 |-  ( V X. V ) C_ ( _V X. _V )
21 sstr2 
 |-  ( t C_ ( V X. V ) -> ( ( V X. V ) C_ ( _V X. _V ) -> t C_ ( _V X. _V ) ) )
22 20 21 mpi 
 |-  ( t C_ ( V X. V ) -> t C_ ( _V X. _V ) )
23 df-rel 
 |-  ( Rel t <-> t C_ ( _V X. _V ) )
24 22 23 sylibr 
 |-  ( t C_ ( V X. V ) -> Rel t )
25 24 adantl 
 |-  ( ( V e. W /\ t C_ ( V X. V ) ) -> Rel t )
26 dfrel4v 
 |-  ( Rel t <-> t = { <. x , y >. | x t y } )
27 nfv 
 |-  F/ x ( V e. W /\ t C_ ( V X. V ) )
28 nfra1 
 |-  F/ x A. x e. V A. y e. V ( x t y <-> y t x )
29 27 28 nfan 
 |-  F/ x ( ( V e. W /\ t C_ ( V X. V ) ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) )
30 nfv 
 |-  F/ y ( V e. W /\ t C_ ( V X. V ) )
31 nfra2w 
 |-  F/ y A. x e. V A. y e. V ( x t y <-> y t x )
32 30 31 nfan 
 |-  F/ y ( ( V e. W /\ t C_ ( V X. V ) ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) )
33 11 sprsymrelfolem2 
 |-  ( ( V e. W /\ t C_ ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) -> ( x t y <-> E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } ) )
34 33 3expa 
 |-  ( ( ( V e. W /\ t C_ ( V X. V ) ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) -> ( x t y <-> E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } ) )
35 29 32 34 opabbid 
 |-  ( ( ( V e. W /\ t C_ ( V X. V ) ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) -> { <. x , y >. | x t y } = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } )
36 35 eqeq2d 
 |-  ( ( ( V e. W /\ t C_ ( V X. V ) ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) -> ( t = { <. x , y >. | x t y } <-> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) )
37 36 biimpd 
 |-  ( ( ( V e. W /\ t C_ ( V X. V ) ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) -> ( t = { <. x , y >. | x t y } -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) )
38 37 ex 
 |-  ( ( V e. W /\ t C_ ( V X. V ) ) -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> ( t = { <. x , y >. | x t y } -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) ) )
39 38 com23 
 |-  ( ( V e. W /\ t C_ ( V X. V ) ) -> ( t = { <. x , y >. | x t y } -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) ) )
40 26 39 syl5bi 
 |-  ( ( V e. W /\ t C_ ( V X. V ) ) -> ( Rel t -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) ) )
41 25 40 mpd 
 |-  ( ( V e. W /\ t C_ ( V X. V ) ) -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) )
42 41 expcom 
 |-  ( t C_ ( V X. V ) -> ( V e. W -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) ) )
43 42 com23 
 |-  ( t C_ ( V X. V ) -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> ( V e. W -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) ) )
44 19 43 sylbi 
 |-  ( t e. ~P ( V X. V ) -> ( A. x e. V A. y e. V ( x t y <-> y t x ) -> ( V e. W -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } ) ) )
45 44 imp31 
 |-  ( ( ( t e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) /\ V e. W ) -> t = { <. x , y >. | E. c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a t b ) } c = { x , y } } )
46 14 18 45 rspcedvd 
 |-  ( ( ( t e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) /\ V e. W ) -> E. f e. P t = { <. x , y >. | E. c e. f c = { x , y } } )
47 46 ex 
 |-  ( ( t e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x t y <-> y t x ) ) -> ( V e. W -> E. f e. P t = { <. x , y >. | E. c e. f c = { x , y } } ) )
48 10 47 sylbi 
 |-  ( t e. R -> ( V e. W -> E. f e. P t = { <. x , y >. | E. c e. f c = { x , y } } ) )
49 48 impcom 
 |-  ( ( V e. W /\ t e. R ) -> E. f e. P t = { <. x , y >. | E. c e. f c = { x , y } } )
50 1 2 3 sprsymrelfv 
 |-  ( f e. P -> ( F ` f ) = { <. x , y >. | E. c e. f c = { x , y } } )
51 50 adantl 
 |-  ( ( ( V e. W /\ t e. R ) /\ f e. P ) -> ( F ` f ) = { <. x , y >. | E. c e. f c = { x , y } } )
52 51 eqeq2d 
 |-  ( ( ( V e. W /\ t e. R ) /\ f e. P ) -> ( t = ( F ` f ) <-> t = { <. x , y >. | E. c e. f c = { x , y } } ) )
53 52 rexbidva 
 |-  ( ( V e. W /\ t e. R ) -> ( E. f e. P t = ( F ` f ) <-> E. f e. P t = { <. x , y >. | E. c e. f c = { x , y } } ) )
54 49 53 mpbird 
 |-  ( ( V e. W /\ t e. R ) -> E. f e. P t = ( F ` f ) )
55 54 ralrimiva 
 |-  ( V e. W -> A. t e. R E. f e. P t = ( F ` f ) )
56 dffo3 
 |-  ( F : P -onto-> R <-> ( F : P --> R /\ A. t e. R E. f e. P t = ( F ` f ) ) )
57 5 55 56 sylanbrc 
 |-  ( V e. W -> F : P -onto-> R )