Theorem harinf

Description: The Hartogs number of an infinite set is at least _om .MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015)

	Ref	Expression
Assertion	harinf	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) → ω ⊆ ( har ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
2	1	adantl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → 𝑥 ∈ On )
3		simplr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → ¬ 𝑆 ∈ Fin )
4		nnfi	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
5	4	adantl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → 𝑥 ∈ Fin )
6		sdomdom	⊢ ( 𝑆 ≺ 𝑥 → 𝑆 ≼ 𝑥 )
7		domfi	⊢ ( ( 𝑥 ∈ Fin ∧ 𝑆 ≼ 𝑥 ) → 𝑆 ∈ Fin )
8	7	ex	⊢ ( 𝑥 ∈ Fin → ( 𝑆 ≼ 𝑥 → 𝑆 ∈ Fin ) )
9	5 6 8	syl2im	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → ( 𝑆 ≺ 𝑥 → 𝑆 ∈ Fin ) )
10	3 9	mtod	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → ¬ 𝑆 ≺ 𝑥 )
11		simpll	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → 𝑆 ∈ 𝑉 )
12		fidomtri	⊢ ( ( 𝑥 ∈ Fin ∧ 𝑆 ∈ 𝑉 ) → ( 𝑥 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑥 ) )
13	5 11 12	syl2anc	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → ( 𝑥 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑥 ) )
14	10 13	mpbird	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → 𝑥 ≼ 𝑆 )
15		elharval	⊢ ( 𝑥 ∈ ( har ‘ 𝑆 ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ≼ 𝑆 ) )
16	2 14 15	sylanbrc	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ω ) → 𝑥 ∈ ( har ‘ 𝑆 ) )
17	16	ex	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) → ( 𝑥 ∈ ω → 𝑥 ∈ ( har ‘ 𝑆 ) ) )
18	17	ssrdv	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin ) → ω ⊆ ( har ‘ 𝑆 ) )