This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bren

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998) Extract breng as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024)

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 eqeltrrdi ⊢ ( 𝑓 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 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ V )
13 7 12 jca ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
14 13 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
15 breng ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
16 1 14 15 pm5.21nii ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )