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

Metamath Proof Explorer

Theorem ener

Description: Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998) (Revised by Mario Carneiro, 15-Nov-2014) (Proof shortened by AV, 1-May-2021)

Ref Expression
Assertion ener ≈ Er V

Proof

Step Hyp Ref Expression
1 relen ⊢ Rel ≈
2 bren ⊢ ( 𝑥 ≈ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 )
3 vex ⊢ 𝑦 ∈ V
4 vex ⊢ 𝑥 ∈ V
5 f1ocnv ⊢ ( 𝑓 : 𝑥 –1-1-onto→ 𝑦 → ◡ 𝑓 : 𝑦 –1-1-onto→ 𝑥 )
6 f1oen2g ⊢ ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ∧ ◡ 𝑓 : 𝑦 –1-1-onto→ 𝑥 ) → 𝑦 ≈ 𝑥 )
7 3 4 5 6 mp3an12i ⊢ ( 𝑓 : 𝑥 –1-1-onto→ 𝑦 → 𝑦 ≈ 𝑥 )
8 7 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 → 𝑦 ≈ 𝑥 )
9 2 8 sylbi ⊢ ( 𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥 )
10 bren ⊢ ( 𝑥 ≈ 𝑦 ↔ ∃ 𝑔 𝑔 : 𝑥 –1-1-onto→ 𝑦 )
11 bren ⊢ ( 𝑦 ≈ 𝑧 ↔ ∃ 𝑓 𝑓 : 𝑦 –1-1-onto→ 𝑧 )
12 exdistrv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝑥 –1-1-onto→ 𝑦 ∧ 𝑓 : 𝑦 –1-1-onto→ 𝑧 ) ↔ ( ∃ 𝑔 𝑔 : 𝑥 –1-1-onto→ 𝑦 ∧ ∃ 𝑓 𝑓 : 𝑦 –1-1-onto→ 𝑧 ) )
13 vex ⊢ 𝑧 ∈ V
14 f1oco ⊢ ( ( 𝑓 : 𝑦 –1-1-onto→ 𝑧 ∧ 𝑔 : 𝑥 –1-1-onto→ 𝑦 ) → ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1-onto→ 𝑧 )
15 14 ancoms ⊢ ( ( 𝑔 : 𝑥 –1-1-onto→ 𝑦 ∧ 𝑓 : 𝑦 –1-1-onto→ 𝑧 ) → ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1-onto→ 𝑧 )
16 f1oen2g ⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ∧ ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1-onto→ 𝑧 ) → 𝑥 ≈ 𝑧 )
17 4 13 15 16 mp3an12i ⊢ ( ( 𝑔 : 𝑥 –1-1-onto→ 𝑦 ∧ 𝑓 : 𝑦 –1-1-onto→ 𝑧 ) → 𝑥 ≈ 𝑧 )
18 17 exlimivv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝑥 –1-1-onto→ 𝑦 ∧ 𝑓 : 𝑦 –1-1-onto→ 𝑧 ) → 𝑥 ≈ 𝑧 )
19 12 18 sylbir ⊢ ( ( ∃ 𝑔 𝑔 : 𝑥 –1-1-onto→ 𝑦 ∧ ∃ 𝑓 𝑓 : 𝑦 –1-1-onto→ 𝑧 ) → 𝑥 ≈ 𝑧 )
20 10 11 19 syl2anb ⊢ ( ( 𝑥 ≈ 𝑦 ∧ 𝑦 ≈ 𝑧 ) → 𝑥 ≈ 𝑧 )
21 4 enref ⊢ 𝑥 ≈ 𝑥
22 4 21 2th ⊢ ( 𝑥 ∈ V ↔ 𝑥 ≈ 𝑥 )
23 1 9 20 22 iseri ⊢ ≈ Er V