Theorem ord0eln0

Description: A nonempty ordinal contains the empty set. Lemma 1.10 of Schloeder p. 2. (Contributed by NM, 25-Nov-1995)

	Ref	Expression
Assertion	ord0eln0	|- ( Ord A -> ( (/) e. A <-> A =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		ne0i	|- ( (/) e. A -> A =/= (/) )
2		ord0	|- Ord (/)
3		noel	|- -. A e. (/)
4		ordtri2	|- ( ( Ord A /\ Ord (/) ) -> ( A e. (/) <-> -. ( A = (/) \/ (/) e. A ) ) )
5	4	con2bid	|- ( ( Ord A /\ Ord (/) ) -> ( ( A = (/) \/ (/) e. A ) <-> -. A e. (/) ) )
6	3 5	mpbiri	|- ( ( Ord A /\ Ord (/) ) -> ( A = (/) \/ (/) e. A ) )
7	2 6	mpan2	|- ( Ord A -> ( A = (/) \/ (/) e. A ) )
8		neor	|- ( ( A = (/) \/ (/) e. A ) <-> ( A =/= (/) -> (/) e. A ) )
9	7 8	sylib	|- ( Ord A -> ( A =/= (/) -> (/) e. A ) )
10	1 9	impbid2	|- ( Ord A -> ( (/) e. A <-> A =/= (/) ) )