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		r1fnon	⊢ 𝑅1 Fn On
7	6	fndmi	⊢ dom 𝑅1 = On
8	7	eleq2i	⊢ ( ω ∈ dom 𝑅1 ↔ ω ∈ On )
9		rankonid	⊢ ( ω ∈ dom 𝑅1 ↔ ( rank ‘ ω ) = ω )
10	8 9	bitr3i	⊢ ( ω ∈ On ↔ ( rank ‘ ω ) = ω )
11	5 10	sylib	⊢ ( ω ∈ HF → ( rank ‘ ω ) = ω )
12	11	eleq1d	⊢ ( ω ∈ HF → ( ( rank ‘ ω ) ∈ ω ↔ ω ∈ ω ) )
13	2 12	bitrd	⊢ ( ω ∈ HF → ( ω ∈ HF ↔ ω ∈ ω ) )
14	1 13	mtbiri	⊢ ( ω ∈ HF → ¬ ω ∈ HF )
15	14	pm2.01i	⊢ ¬ ω ∈ HF