Metamath Proof Explorer

Theorem sprsymrelf1

Description: The mapping F is a one-to-one 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 sprsymrelf1 
|- F : P -1-1-> 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 1 2 3 sprsymrelfv 
 |-  ( a e. P -> ( F ` a ) = { <. x , y >. | E. c e. a c = { x , y } } )
6 1 2 3 sprsymrelfv 
 |-  ( b e. P -> ( F ` b ) = { <. x , y >. | E. c e. b c = { x , y } } )
7 5 6 eqeqan12d 
 |-  ( ( a e. P /\ b e. P ) -> ( ( F ` a ) = ( F ` b ) <-> { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) )
8 1 eleq2i 
 |-  ( a e. P <-> a e. ~P ( Pairs ` V ) )
9 vex 
 |-  a e. _V
10 9 elpw 
 |-  ( a e. ~P ( Pairs ` V ) <-> a C_ ( Pairs ` V ) )
11 8 10 bitri 
 |-  ( a e. P <-> a C_ ( Pairs ` V ) )
12 1 eleq2i 
 |-  ( b e. P <-> b e. ~P ( Pairs ` V ) )
13 vex 
 |-  b e. _V
14 13 elpw 
 |-  ( b e. ~P ( Pairs ` V ) <-> b C_ ( Pairs ` V ) )
15 12 14 bitri 
 |-  ( b e. P <-> b C_ ( Pairs ` V ) )
16 sprsymrelf1lem 
 |-  ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> a C_ b ) )
17 16 imp 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) -> a C_ b )
18 eqcom 
 |-  ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } <-> { <. x , y >. | E. c e. b c = { x , y } } = { <. x , y >. | E. c e. a c = { x , y } } )
19 sprsymrelf1lem 
 |-  ( ( b C_ ( Pairs ` V ) /\ a C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. b c = { x , y } } = { <. x , y >. | E. c e. a c = { x , y } } -> b C_ a ) )
20 18 19 syl5bi 
 |-  ( ( b C_ ( Pairs ` V ) /\ a C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> b C_ a ) )
21 20 ancoms 
 |-  ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> b C_ a ) )
22 21 imp 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) -> b C_ a )
23 17 22 eqssd 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) -> a = b )
24 23 ex 
 |-  ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> a = b ) )
25 11 15 24 syl2anb 
 |-  ( ( a e. P /\ b e. P ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> a = b ) )
26 7 25 sylbid 
 |-  ( ( a e. P /\ b e. P ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) )
27 26 rgen2 
 |-  A. a e. P A. b e. P ( ( F ` a ) = ( F ` b ) -> a = b )
28 dff13 
 |-  ( F : P -1-1-> R <-> ( F : P --> R /\ A. a e. P A. b e. P ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
29 4 27 28 mpbir2an 
 |-  F : P -1-1-> R