Theorem bren

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998)

	Ref	Expression
Assertion	bren	⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		encv	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
2		f1ofn	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 Fn 𝐴 )
3		fndm	⊢ ( 𝑓 Fn 𝐴 → dom 𝑓 = 𝐴 )
4		vex	⊢ 𝑓 ∈ V
5	4	dmex	⊢ dom 𝑓 ∈ V
6	3 5	syl6eqelr	⊢ ( 𝑓 Fn 𝐴 → 𝐴 ∈ V )
7	2 6	syl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐴 ∈ V )
8		f1ofo	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
9		forn	⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ran 𝑓 = 𝐵 )
10	8 9	syl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ran 𝑓 = 𝐵 )
11	4	rnex	⊢ ran 𝑓 ∈ V
12	10 11	syl6eqelr	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ V )
13	7 12	jca	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
14	13	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
15		f1oeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑥 –1-1-onto→ 𝑦 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝑦 ) )
16	15	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑦 ) )
17		f1oeq3	⊢ ( 𝑦 = 𝐵 → ( 𝑓 : 𝐴 –1-1-onto→ 𝑦 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
18	17	exbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
19		df-en	⊢ ≈ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 }
20	16 18 19	brabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
21	1 14 20	pm5.21nii	⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )