brenOLD

Description: Obsolete version of bren as of 23-Sep-2024. (Contributed by NM, 15-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	brenOLD	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		encv	$⊢ A \approx B \to (A \in V \land B \in V)$
2		f1ofn	$⊢ f : A \underset{1-1 onto}{⟶} B \to f Fn A$
3		fndm	$⊢ f Fn A \to dom f = A$
4		vex	$⊢ f \in V$
5	4	dmex	$⊢ dom f \in V$
6	3 5	eqeltrrdi	$⊢ f Fn A \to A \in V$
7	2 6	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to A \in V$
8		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
9		forn	$⊢ f : A \underset{onto}{⟶} B \to ran f = B$
10	8 9	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to ran f = B$
11	4	rnex	$⊢ ran f \in V$
12	10 11	eqeltrrdi	$⊢ f : A \underset{1-1 onto}{⟶} B \to B \in V$
13	7 12	jca	$⊢ f : A \underset{1-1 onto}{⟶} B \to (A \in V \land B \in V)$
14	13	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} B \to (A \in V \land B \in V)$
15		f1oeq2	$⊢ x = A \to (f : x \underset{1-1 onto}{⟶} y \leftrightarrow f : A \underset{1-1 onto}{⟶} y)$
16	15	exbidv	$⊢ x = A \to (\exists f f : x \underset{1-1 onto}{⟶} y \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} y)$
17		f1oeq3	$⊢ y = B \to (f : A \underset{1-1 onto}{⟶} y \leftrightarrow f : A \underset{1-1 onto}{⟶} B)$
18	17	exbidv	$⊢ y = B \to (\exists f f : A \underset{1-1 onto}{⟶} y \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B)$
19		df-en	$⊢ \approx = \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\}$
20	16 18 19	brabg	$⊢ (A \in V \land B \in V) \to (A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B)$
21	1 14 20	pm5.21nii	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem brenOLD

Proof