Theorem dom0

Description: A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	dom0	⊢ ( 𝐴 ≼ ∅ ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		brdomi	⊢ ( 𝐴 ≼ ∅ → ∃ 𝑓 𝑓 : 𝐴 –1-1→ ∅ )
2		f1f	⊢ ( 𝑓 : 𝐴 –1-1→ ∅ → 𝑓 : 𝐴 ⟶ ∅ )
3		f00	⊢ ( 𝑓 : 𝐴 ⟶ ∅ ↔ ( 𝑓 = ∅ ∧ 𝐴 = ∅ ) )
4	3	simprbi	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → 𝐴 = ∅ )
5	2 4	syl	⊢ ( 𝑓 : 𝐴 –1-1→ ∅ → 𝐴 = ∅ )
6	5	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ ∅ → 𝐴 = ∅ )
7	1 6	syl	⊢ ( 𝐴 ≼ ∅ → 𝐴 = ∅ )
8		en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
9		endom	⊢ ( 𝐴 ≈ ∅ → 𝐴 ≼ ∅ )
10	8 9	sylbir	⊢ ( 𝐴 = ∅ → 𝐴 ≼ ∅ )
11	7 10	impbii	⊢ ( 𝐴 ≼ ∅ ↔ 𝐴 = ∅ )