Theorem infn0

Description: An infinite set is not empty. (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	infn0	|- ( _om ~<_ A -> A =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		peano1	|- (/) e. _om
2		infsdomnn	|- ( ( _om ~<_ A /\ (/) e. _om ) -> (/) ~< A )
3	1 2	mpan2	|- ( _om ~<_ A -> (/) ~< A )
4		reldom	|- Rel ~<_
5	4	brrelex2i	|- ( _om ~<_ A -> A e. _V )
6		0sdomg	|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
7	5 6	syl	|- ( _om ~<_ A -> ( (/) ~< A <-> A =/= (/) ) )
8	3 7	mpbid	|- ( _om ~<_ A -> A =/= (/) )