Metamath Proof Explorer

Theorem en3d

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 12-May-2014) (Revised by AV, 4-Aug-2024)

		Ref	Expression
	Hypotheses	en3d.1	$⊢ φ \to A \in V$
		en3d.2	$⊢ φ \to B \in W$
		en3d.3	$⊢ φ \to (x \in A \to C \in B)$
		en3d.4	$⊢ φ \to (y \in B \to D \in A)$
		en3d.5	$⊢ φ \to ((x \in A \land y \in B) \to (x = D \leftrightarrow y = C))$
	Assertion	en3d	$⊢ φ \to A \approx B$

Proof

Step	Hyp	Ref	Expression
1		en3d.1	$⊢ φ \to A \in V$
2		en3d.2	$⊢ φ \to B \in W$
3		en3d.3	$⊢ φ \to (x \in A \to C \in B)$
4		en3d.4	$⊢ φ \to (y \in B \to D \in A)$
5		en3d.5	$⊢ φ \to ((x \in A \land y \in B) \to (x = D \leftrightarrow y = C))$
6		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
7	3	imp	$⊢ (φ \land x \in A) \to C \in B$
8	4	imp	$⊢ (φ \land y \in B) \to D \in A$
9	5	imp	$⊢ (φ \land (x \in A \land y \in B)) \to (x = D \leftrightarrow y = C)$
10	6 7 8 9	f1o2d	$⊢ φ \to (x \in A ⟼ C) : A \underset{1-1 onto}{⟶} B$
11		f1oen2g	$⊢ (A \in V \land B \in W \land (x \in A ⟼ C) : A \underset{1-1 onto}{⟶} B) \to A \approx B$
12	1 2 10 11	syl3anc	$⊢ φ \to A \approx B$