Metamath Proof Explorer

Theorem sprsymrelf

Description: The mapping F is a function from the subsets of the set of pairs over a fixed set V into the symmetric relations R on the fixed set V . (Contributed by AV, 19-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 sprsymrelf 
|- F : P --> 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 sprsymrelfvlem 
 |-  ( p C_ ( Pairs ` V ) -> { <. x , y >. | E. c e. p c = { x , y } } e. ~P ( V X. V ) )
5 prcom 
 |-  { x , y } = { y , x }
6 5 a1i 
 |-  ( ( ( p C_ ( Pairs ` V ) /\ ( x e. V /\ y e. V ) ) /\ c e. p ) -> { x , y } = { y , x } )
7 6 eqeq2d 
 |-  ( ( ( p C_ ( Pairs ` V ) /\ ( x e. V /\ y e. V ) ) /\ c e. p ) -> ( c = { x , y } <-> c = { y , x } ) )
8 7 rexbidva 
 |-  ( ( p C_ ( Pairs ` V ) /\ ( x e. V /\ y e. V ) ) -> ( E. c e. p c = { x , y } <-> E. c e. p c = { y , x } ) )
9 df-br 
 |-  ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> <. x , y >. e. { <. x , y >. | E. c e. p c = { x , y } } )
10 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | E. c e. p c = { x , y } } <-> E. c e. p c = { x , y } )
11 9 10 bitri 
 |-  ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> E. c e. p c = { x , y } )
12 vex 
 |-  y e. _V
13 vex 
 |-  x e. _V
14 preq12 
 |-  ( ( a = y /\ b = x ) -> { a , b } = { y , x } )
15 14 eqeq2d 
 |-  ( ( a = y /\ b = x ) -> ( c = { a , b } <-> c = { y , x } ) )
16 15 rexbidv 
 |-  ( ( a = y /\ b = x ) -> ( E. c e. p c = { a , b } <-> E. c e. p c = { y , x } ) )
17 preq12 
 |-  ( ( x = a /\ y = b ) -> { x , y } = { a , b } )
18 17 eqeq2d 
 |-  ( ( x = a /\ y = b ) -> ( c = { x , y } <-> c = { a , b } ) )
19 18 rexbidv 
 |-  ( ( x = a /\ y = b ) -> ( E. c e. p c = { x , y } <-> E. c e. p c = { a , b } ) )
20 19 cbvopabv 
 |-  { <. x , y >. | E. c e. p c = { x , y } } = { <. a , b >. | E. c e. p c = { a , b } }
21 12 13 16 20 braba 
 |-  ( y { <. x , y >. | E. c e. p c = { x , y } } x <-> E. c e. p c = { y , x } )
22 8 11 21 3bitr4g 
 |-  ( ( p C_ ( Pairs ` V ) /\ ( x e. V /\ y e. V ) ) -> ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) )
23 22 ralrimivva 
 |-  ( p C_ ( Pairs ` V ) -> A. x e. V A. y e. V ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) )
24 4 23 jca 
 |-  ( p C_ ( Pairs ` V ) -> ( { <. x , y >. | E. c e. p c = { x , y } } e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) ) )
25 1 eleq2i 
 |-  ( p e. P <-> p e. ~P ( Pairs ` V ) )
26 vex 
 |-  p e. _V
27 26 elpw 
 |-  ( p e. ~P ( Pairs ` V ) <-> p C_ ( Pairs ` V ) )
28 25 27 bitri 
 |-  ( p e. P <-> p C_ ( Pairs ` V ) )
29 nfopab1 
 |-  F/_ x { <. x , y >. | E. c e. p c = { x , y } }
30 29 nfeq2 
 |-  F/ x r = { <. x , y >. | E. c e. p c = { x , y } }
31 nfopab2 
 |-  F/_ y { <. x , y >. | E. c e. p c = { x , y } }
32 31 nfeq2 
 |-  F/ y r = { <. x , y >. | E. c e. p c = { x , y } }
33 breq 
 |-  ( r = { <. x , y >. | E. c e. p c = { x , y } } -> ( x r y <-> x { <. x , y >. | E. c e. p c = { x , y } } y ) )
34 breq 
 |-  ( r = { <. x , y >. | E. c e. p c = { x , y } } -> ( y r x <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) )
35 33 34 bibi12d 
 |-  ( r = { <. x , y >. | E. c e. p c = { x , y } } -> ( ( x r y <-> y r x ) <-> ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) ) )
36 32 35 ralbid 
 |-  ( r = { <. x , y >. | E. c e. p c = { x , y } } -> ( A. y e. V ( x r y <-> y r x ) <-> A. y e. V ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) ) )
37 30 36 ralbid 
 |-  ( r = { <. x , y >. | E. c e. p c = { x , y } } -> ( A. x e. V A. y e. V ( x r y <-> y r x ) <-> A. x e. V A. y e. V ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) ) )
38 37 elrab 
 |-  ( { <. x , y >. | E. c e. p c = { x , y } } e. { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) } <-> ( { <. x , y >. | E. c e. p c = { x , y } } e. ~P ( V X. V ) /\ A. x e. V A. y e. V ( x { <. x , y >. | E. c e. p c = { x , y } } y <-> y { <. x , y >. | E. c e. p c = { x , y } } x ) ) )
39 24 28 38 3imtr4i 
 |-  ( p e. P -> { <. x , y >. | E. c e. p c = { x , y } } e. { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) } )
40 39 2 eleqtrrdi 
 |-  ( p e. P -> { <. x , y >. | E. c e. p c = { x , y } } e. R )
41 3 40 fmpti 
 |-  F : P --> R