Theorem ord0eln0

Description: A nonempty ordinal contains the empty set. (Contributed by NM, 25-Nov-1995)

	Ref	Expression
Assertion	ord0eln0	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( ∅ ∈ 𝐴 → 𝐴 ≠ ∅ )
2		ord0	⊢ Ord ∅
3		noel	⊢ ¬ 𝐴 ∈ ∅
4		ordtri2	⊢ ( ( Ord 𝐴 ∧ Ord ∅ ) → ( 𝐴 ∈ ∅ ↔ ¬ ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) ) )
5	4	con2bid	⊢ ( ( Ord 𝐴 ∧ Ord ∅ ) → ( ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) ↔ ¬ 𝐴 ∈ ∅ ) )
6	3 5	mpbiri	⊢ ( ( Ord 𝐴 ∧ Ord ∅ ) → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
7	2 6	mpan2	⊢ ( Ord 𝐴 → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
8		neor	⊢ ( ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ≠ ∅ → ∅ ∈ 𝐴 ) )
9	7 8	sylib	⊢ ( Ord 𝐴 → ( 𝐴 ≠ ∅ → ∅ ∈ 𝐴 ) )
10	1 9	impbid2	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )