Theorem infn0

Description: An infinite set is not empty. For a shorter proof using ax-un , see infn0ALT . (Contributed by NM, 23-Oct-2004) Avoid ax-un . (Revised by BTernaryTau, 8-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		brdomi	|- ( _om ~<_ A -> E. f f : _om -1-1-> A )
2		peano1	|- (/) e. _om
3		f1f1orn	|- ( f : _om -1-1-> A -> f : _om -1-1-onto-> ran f )
4	3	adantr	|- ( ( f : _om -1-1-> A /\ A = (/) ) -> f : _om -1-1-onto-> ran f )
5		f1f	|- ( f : _om -1-1-> A -> f : _om --> A )
6	5	frnd	|- ( f : _om -1-1-> A -> ran f C_ A )
7		sseq0	|- ( ( ran f C_ A /\ A = (/) ) -> ran f = (/) )
8	6 7	sylan	|- ( ( f : _om -1-1-> A /\ A = (/) ) -> ran f = (/) )
9	8	f1oeq3d	|- ( ( f : _om -1-1-> A /\ A = (/) ) -> ( f : _om -1-1-onto-> ran f <-> f : _om -1-1-onto-> (/) ) )
10	4 9	mpbid	|- ( ( f : _om -1-1-> A /\ A = (/) ) -> f : _om -1-1-onto-> (/) )
11		f1ocnv	|- ( f : _om -1-1-onto-> (/) -> `' f : (/) -1-1-onto-> _om )
12		noel	|- -. (/) e. (/)
13		f1o00	|- ( `' f : (/) -1-1-onto-> _om <-> ( `' f = (/) /\ _om = (/) ) )
14	13	simprbi	|- ( `' f : (/) -1-1-onto-> _om -> _om = (/) )
15	14	eleq2d	|- ( `' f : (/) -1-1-onto-> _om -> ( (/) e. _om <-> (/) e. (/) ) )
16	12 15	mtbiri	|- ( `' f : (/) -1-1-onto-> _om -> -. (/) e. _om )
17	10 11 16	3syl	|- ( ( f : _om -1-1-> A /\ A = (/) ) -> -. (/) e. _om )
18	2 17	mt2	|- -. ( f : _om -1-1-> A /\ A = (/) )
19	18	imnani	|- ( f : _om -1-1-> A -> -. A = (/) )
20	19	neqned	|- ( f : _om -1-1-> A -> A =/= (/) )
21	20	exlimiv	|- ( E. f f : _om -1-1-> A -> A =/= (/) )
22	1 21	syl	|- ( _om ~<_ A -> A =/= (/) )