Theorem hfninf

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

	Ref	Expression
Assertion	hfninf	⊢ ¬ ω ∈ Hf

Proof

Step	Hyp	Ref	Expression
1		elirr	⊢ ¬ ω ∈ ω
2		elhf2g	⊢ ( ω ∈ Hf → ( ω ∈ Hf ↔ ( rank ‘ ω ) ∈ ω ) )
3		ordom	⊢ Ord ω
4		elong	⊢ ( ω ∈ Hf → ( ω ∈ On ↔ Ord ω ) )
5	3 4	mpbiri	⊢ ( ω ∈ Hf → ω ∈ On )
6		r111	⊢ 𝑅1 : On –1-1→ V
7		f1dm	⊢ ( 𝑅1 : On –1-1→ V → dom 𝑅1 = On )
8	6 7	ax-mp	⊢ dom 𝑅1 = On
9	8	eleq2i	⊢ ( ω ∈ dom 𝑅1 ↔ ω ∈ On )
10		rankonid	⊢ ( ω ∈ dom 𝑅1 ↔ ( rank ‘ ω ) = ω )
11	9 10	bitr3i	⊢ ( ω ∈ On ↔ ( rank ‘ ω ) = ω )
12	5 11	sylib	⊢ ( ω ∈ Hf → ( rank ‘ ω ) = ω )
13	12	eleq1d	⊢ ( ω ∈ Hf → ( ( rank ‘ ω ) ∈ ω ↔ ω ∈ ω ) )
14	2 13	bitrd	⊢ ( ω ∈ Hf → ( ω ∈ Hf ↔ ω ∈ ω ) )
15	1 14	mtbiri	⊢ ( ω ∈ Hf → ¬ ω ∈ Hf )
16		pm2.01	⊢ ( ( ω ∈ Hf → ¬ ω ∈ Hf ) → ¬ ω ∈ Hf )
17	15 16	ax-mp	⊢ ¬ ω ∈ Hf