hfninf

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

		Ref	Expression
	Assertion	hfninf	$⊢ \neg ω \in Hf$

Step	Hyp	Ref	Expression
1		elirr	$⊢ \neg ω \in ω$
2		elhf2g	$⊢ ω \in Hf \to (ω \in Hf \leftrightarrow rank (ω) \in ω)$
3		ordom	$⊢ Ord ω$
4		elong	$⊢ ω \in Hf \to (ω \in On \leftrightarrow Ord ω)$
5	3 4	mpbiri	$⊢ ω \in Hf \to ω \in On$
6		r111	$⊢ R_{1} : On \underset{1-1}{⟶} V$
7		f1dm	$⊢ R_{1} : On \underset{1-1}{⟶} V \to dom R_{1} = On$
8	6 7	ax-mp	$⊢ dom R_{1} = On$
9	8	eleq2i	$⊢ ω \in dom R_{1} \leftrightarrow ω \in On$
10		rankonid	$⊢ ω \in dom R_{1} \leftrightarrow rank (ω) = ω$
11	9 10	bitr3i	$⊢ ω \in On \leftrightarrow rank (ω) = ω$
12	5 11	sylib	$⊢ ω \in Hf \to rank (ω) = ω$
13	12	eleq1d	$⊢ ω \in Hf \to (rank (ω) \in ω \leftrightarrow ω \in ω)$
14	2 13	bitrd	$⊢ ω \in Hf \to (ω \in Hf \leftrightarrow ω \in ω)$
15	1 14	mtbiri	$⊢ ω \in Hf \to \neg ω \in Hf$
16		pm2.01	$⊢ (ω \in Hf \to \neg ω \in Hf) \to \neg ω \in Hf$
17	15 16	ax-mp	$⊢ \neg ω \in Hf$

Metamath Proof Explorer