Theorem hfninf

Description: _om is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	hfninf	|- -. _om e. HF

Proof

Step	Hyp	Ref	Expression
1		elirr	|- -. _om e. _om
2		elhf2g	|- ( _om e. HF -> ( _om e. HF <-> ( rank ` _om ) e. _om ) )
3		ordom	|- Ord _om
4		elong	|- ( _om e. HF -> ( _om e. On <-> Ord _om ) )
5	3 4	mpbiri	|- ( _om e. HF -> _om e. On )
6		r1fnon	|- R1 Fn On
7	6	fndmi	|- dom R1 = On
8	7	eleq2i	|- ( _om e. dom R1 <-> _om e. On )
9		rankonid	|- ( _om e. dom R1 <-> ( rank ` _om ) = _om )
10	8 9	bitr3i	|- ( _om e. On <-> ( rank ` _om ) = _om )
11	5 10	sylib	|- ( _om e. HF -> ( rank ` _om ) = _om )
12	11	eleq1d	|- ( _om e. HF -> ( ( rank ` _om ) e. _om <-> _om e. _om ) )
13	2 12	bitrd	|- ( _om e. HF -> ( _om e. HF <-> _om e. _om ) )
14	1 13	mtbiri	|- ( _om e. HF -> -. _om e. HF )
15	14	pm2.01i	|- -. _om e. HF