Theorem hfninf

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

	Ref	Expression
Assertion	hfninf	Could not format assertion : No typesetting found for |- -. _om e. HF with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elirr	$$⊢\neg \mathrm{\omega }\in \mathrm{\omega }$$
2		elhf2g	Could not format ( _om e. HF -> ( _om e. HF <-> ( rank ` _om ) e. _om ) ) : No typesetting found for |- ( _om e. HF -> ( _om e. HF <-> ( rank ` _om ) e. _om ) ) with typecode |-
3		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
4		elong	Could not format ( _om e. HF -> ( _om e. On <-> Ord _om ) ) : No typesetting found for |- ( _om e. HF -> ( _om e. On <-> Ord _om ) ) with typecode |-
5	3 4	mpbiri	Could not format ( _om e. HF -> _om e. On ) : No typesetting found for |- ( _om e. HF -> _om e. On ) with typecode |-
6		r1fnon	$$⊢R_{1}Fn\mathrm{On}$$
7	6	fndmi	$$⊢\mathrm{dom}{R}_1=\mathrm{On}$$
8	7	eleq2i	$$⊢\mathrm{\omega }\in \mathrm{dom}{R}_1\leftrightarrow \mathrm{\omega }\in \mathrm{On}$$
9		rankonid	$$⊢\mathrm{\omega }\in \mathrm{dom}{R}_1\leftrightarrow \mathrm{rank}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$
10	8 9	bitr3i	$$⊢\mathrm{\omega }\in \mathrm{On}\leftrightarrow \mathrm{rank}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$
11	5 10	sylib	Could not format ( _om e. HF -> ( rank ` _om ) = _om ) : No typesetting found for |- ( _om e. HF -> ( rank ` _om ) = _om ) with typecode |-
12	11	eleq1d	Could not format ( _om e. HF -> ( ( rank ` _om ) e. _om <-> _om e. _om ) ) : No typesetting found for |- ( _om e. HF -> ( ( rank ` _om ) e. _om <-> _om e. _om ) ) with typecode |-
13	2 12	bitrd	Could not format ( _om e. HF -> ( _om e. HF <-> _om e. _om ) ) : No typesetting found for |- ( _om e. HF -> ( _om e. HF <-> _om e. _om ) ) with typecode |-
14	1 13	mtbiri	Could not format ( _om e. HF -> -. _om e. HF ) : No typesetting found for |- ( _om e. HF -> -. _om e. HF ) with typecode |-
15	14	pm2.01i	Could not format -. _om e. HF : No typesetting found for |- -. _om e. HF with typecode |-