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