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 \in V \land \neg S \in Fin) \to ω \subseteq har (S)$

Step	Hyp	Ref	Expression
1		nnon	$⊢ x \in ω \to x \in On$
2	1	adantl	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to x \in On$
3		simplr	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to \neg S \in Fin$
4		nnfi	$⊢ x \in ω \to x \in Fin$
5	4	adantl	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to x \in Fin$
6		sdomdom	$⊢ S ≺ x \to S ≼ x$
7		domfi	$⊢ (x \in Fin \land S ≼ x) \to S \in Fin$
8	7	ex	$⊢ x \in Fin \to (S ≼ x \to S \in Fin)$
9	5 6 8	syl2im	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to (S ≺ x \to S \in Fin)$
10	3 9	mtod	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to \neg S ≺ x$
11		simpll	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to S \in V$
12		fidomtri	$⊢ (x \in Fin \land S \in V) \to (x ≼ S \leftrightarrow \neg S ≺ x)$
13	5 11 12	syl2anc	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to (x ≼ S \leftrightarrow \neg S ≺ x)$
14	10 13	mpbird	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to x ≼ S$
15		elharval	$⊢ x \in har (S) \leftrightarrow (x \in On \land x ≼ S)$
16	2 14 15	sylanbrc	$⊢ ((S \in V \land \neg S \in Fin) \land x \in ω) \to x \in har (S)$
17	16	ex	$⊢ (S \in V \land \neg S \in Fin) \to (x \in ω \to x \in har (S))$
18	17	ssrdv	$⊢ (S \in V \land \neg S \in Fin) \to ω \subseteq har (S)$

Metamath Proof Explorer