Theorem en2prd

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

	Ref	Expression
Hypotheses	en2prd.1	$$⊢\phi \to A\in V$$
	en2prd.2	$$⊢\phi \to B\in W$$
	en2prd.3	$$⊢\phi \to C\in X$$
	en2prd.4	$$⊢\phi \to D\in Y$$
	en2prd.5	$$⊢\phi \to A\ne B$$
	en2prd.6	$$⊢\phi \to C\ne D$$
Assertion	en2prd	$$⊢\phi \to \left\{A,B\right\}\approx \left\{C,D\right\}$$

Proof

Step	Hyp	Ref	Expression
1		en2prd.1	$$⊢\phi \to A\in V$$
2		en2prd.2	$$⊢\phi \to B\in W$$
3		en2prd.3	$$⊢\phi \to C\in X$$
4		en2prd.4	$$⊢\phi \to D\in Y$$
5		en2prd.5	$$⊢\phi \to A\ne B$$
6		en2prd.6	$$⊢\phi \to C\ne D$$
7		prex	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}\in \mathrm{V}$$
8		f1oprg	$$⊢\left(\left(A\in V\wedge C\in X\right)\wedge \left(B\in W\wedge D\in Y\right)\right)\to \left(\left(A\ne B\wedge C\ne D\right)\to \left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\right)$$
9	1 3 2 4 8	syl22anc	$$⊢\phi \to \left(\left(A\ne B\wedge C\ne D\right)\to \left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\right)$$
10	5 6 9	mp2and	$$⊢\phi \to \left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}$$
11		f1oeq1	$$⊢f=\left\{⟨A,C⟩,⟨B,D⟩\right\}\to \left(f:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\leftrightarrow \left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\right)$$
12	11	spcegv	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}\in \mathrm{V}\to \left(\left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\to \exists ff:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\right)$$
13	7 10 12	mpsyl	$$⊢\phi \to \exists ff:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}$$
14		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
15		prex	$$⊢\left\{C,D\right\}\in \mathrm{V}$$
16		breng	$$⊢\left(\left\{A,B\right\}\in \mathrm{V}\wedge \left\{C,D\right\}\in \mathrm{V}\right)\to \left(\left\{A,B\right\}\approx \left\{C,D\right\}\leftrightarrow \exists ff:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}\right)$$
17	14 15 16	mp2an	$$⊢\left\{A,B\right\}\approx \left\{C,D\right\}\leftrightarrow \exists ff:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{C,D\right\}$$
18	13 17	sylibr	$$⊢\phi \to \left\{A,B\right\}\approx \left\{C,D\right\}$$