en2prd

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

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

Metamath Proof Explorer