This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem en2prd

Description: Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024)

Ref Expression
Hypotheses en2prd.1 
|- ( ph -> A e. V )
en2prd.2 
|- ( ph -> B e. W )
en2prd.3 
|- ( ph -> C e. X )
en2prd.4 
|- ( ph -> D e. Y )
en2prd.5 
|- ( ph -> A =/= B )
en2prd.6 
|- ( ph -> C =/= D )
Assertion en2prd 
|- ( ph -> { A , B } ~~ { C , D } )

Proof

Step Hyp Ref Expression
1 en2prd.1 
 |-  ( ph -> A e. V )
2 en2prd.2 
 |-  ( ph -> B e. W )
3 en2prd.3 
 |-  ( ph -> C e. X )
4 en2prd.4 
 |-  ( ph -> D e. Y )
5 en2prd.5 
 |-  ( ph -> A =/= B )
6 en2prd.6 
 |-  ( ph -> C =/= D )
7 prex 
 |-  { <. A , C >. , <. B , D >. } e. _V
8 f1oprg 
 |-  ( ( ( A e. V /\ C e. X ) /\ ( B e. W /\ D e. Y ) ) -> ( ( A =/= B /\ C =/= D ) -> { <. A , C >. , <. B , D >. } : { A , B } -1-1-onto-> { C , D } ) )
9 1 3 2 4 8 syl22anc 
 |-  ( ph -> ( ( A =/= B /\ C =/= D ) -> { <. A , C >. , <. B , D >. } : { A , B } -1-1-onto-> { C , D } ) )
10 5 6 9 mp2and 
 |-  ( ph -> { <. A , C >. , <. B , D >. } : { A , B } -1-1-onto-> { C , D } )
11 f1oeq1 
 |-  ( f = { <. A , C >. , <. B , D >. } -> ( f : { A , B } -1-1-onto-> { C , D } <-> { <. A , C >. , <. B , D >. } : { A , B } -1-1-onto-> { C , D } ) )
12 11 spcegv 
 |-  ( { <. A , C >. , <. B , D >. } e. _V -> ( { <. A , C >. , <. B , D >. } : { A , B } -1-1-onto-> { C , D } -> E. f f : { A , B } -1-1-onto-> { C , D } ) )
13 7 10 12 mpsyl 
 |-  ( ph -> E. f f : { A , B } -1-1-onto-> { C , D } )
14 prex 
 |-  { A , B } e. _V
15 prex 
 |-  { C , D } e. _V
16 breng 
 |-  ( ( { A , B } e. _V /\ { C , D } e. _V ) -> ( { A , B } ~~ { C , D } <-> E. f f : { A , B } -1-1-onto-> { C , D } ) )
17 14 15 16 mp2an 
 |-  ( { A , B } ~~ { C , D } <-> E. f f : { A , B } -1-1-onto-> { C , D } )
18 13 17 sylibr 
 |-  ( ph -> { A , B } ~~ { C , D } )