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	|- ( ( S e. V /\ -. S e. Fin ) -> _om C_ ( har ` S ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( x e. _om -> x e. On )
2	1	adantl	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> x e. On )
3		simplr	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> -. S e. Fin )
4		nnfi	|- ( x e. _om -> x e. Fin )
5	4	adantl	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> x e. Fin )
6		sdomdom	|- ( S ~< x -> S ~<_ x )
7		domfi	|- ( ( x e. Fin /\ S ~<_ x ) -> S e. Fin )
8	7	ex	|- ( x e. Fin -> ( S ~<_ x -> S e. Fin ) )
9	5 6 8	syl2im	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> ( S ~< x -> S e. Fin ) )
10	3 9	mtod	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> -. S ~< x )
11		simpll	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> S e. V )
12		fidomtri	|- ( ( x e. Fin /\ S e. V ) -> ( x ~<_ S <-> -. S ~< x ) )
13	5 11 12	syl2anc	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> ( x ~<_ S <-> -. S ~< x ) )
14	10 13	mpbird	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> x ~<_ S )
15		elharval	|- ( x e. ( har ` S ) <-> ( x e. On /\ x ~<_ S ) )
16	2 14 15	sylanbrc	|- ( ( ( S e. V /\ -. S e. Fin ) /\ x e. _om ) -> x e. ( har ` S ) )
17	16	ex	|- ( ( S e. V /\ -. S e. Fin ) -> ( x e. _om -> x e. ( har ` S ) ) )
18	17	ssrdv	|- ( ( S e. V /\ -. S e. Fin ) -> _om C_ ( har ` S ) )