Theorem en0

Description: The empty set is equinumerous only to itself. Exercise 1 of TakeutiZaring p. 88. (Contributed by NM, 27-May-1998) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 23-Sep-2024)

	Ref	Expression
Assertion	en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		encv	⊢ ( 𝐴 ≈ ∅ → ( 𝐴 ∈ V ∧ ∅ ∈ V ) )
2		breng	⊢ ( ( 𝐴 ∈ V ∧ ∅ ∈ V ) → ( 𝐴 ≈ ∅ ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ ∅ ) )
3	1 2	syl	⊢ ( 𝐴 ≈ ∅ → ( 𝐴 ≈ ∅ ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ ∅ ) )
4	3	ibi	⊢ ( 𝐴 ≈ ∅ → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ ∅ )
5		f1ocnv	⊢ ( 𝑓 : 𝐴 –1-1-onto→ ∅ → ◡ 𝑓 : ∅ –1-1-onto→ 𝐴 )
6		f1o00	⊢ ( ◡ 𝑓 : ∅ –1-1-onto→ 𝐴 ↔ ( ◡ 𝑓 = ∅ ∧ 𝐴 = ∅ ) )
7	6	simprbi	⊢ ( ◡ 𝑓 : ∅ –1-1-onto→ 𝐴 → 𝐴 = ∅ )
8	5 7	syl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ ∅ → 𝐴 = ∅ )
9	8	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ ∅ → 𝐴 = ∅ )
10	4 9	syl	⊢ ( 𝐴 ≈ ∅ → 𝐴 = ∅ )
11		0ex	⊢ ∅ ∈ V
12		f1oeq1	⊢ ( 𝑓 = ∅ → ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
13		f1o0	⊢ ∅ : ∅ –1-1-onto→ ∅
14	11 12 13	ceqsexv2d	⊢ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅
15		breng	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ∅ ≈ ∅ ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅ ) )
16	11 11 15	mp2an	⊢ ( ∅ ≈ ∅ ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅ )
17	14 16	mpbir	⊢ ∅ ≈ ∅
18		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≈ ∅ ↔ ∅ ≈ ∅ ) )
19	17 18	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ≈ ∅ )
20	10 19	impbii	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )