Theorem en2prd

Description: Two 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 } )