wunom

Description: A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Hypothesis	wun0.1	$⊢ φ \to U \in WUni$
	Assertion	wunom	$⊢ φ \to ω \subseteq U$

Step	Hyp	Ref	Expression
1		wun0.1	$⊢ φ \to U \in WUni$
2	1	adantr	$⊢ (φ \land x \in ω) \to U \in WUni$
3	1	wunr1om	$⊢ φ \to R_{1} [ω] \subseteq U$
4		r1fun	$⊢ Fun R_{1}$
5		r1dmlim	$⊢ Lim dom R_{1}$
6		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
7	5 6	ax-mp	$⊢ ω \subseteq dom R_{1}$
8		funimass4	$⊢ (Fun R_{1} \land ω \subseteq dom R_{1}) \to (R_{1} [ω] \subseteq U \leftrightarrow \forall x \in ω R_{1} (x) \in U)$
9	4 7 8	mp2an	$⊢ R_{1} [ω] \subseteq U \leftrightarrow \forall x \in ω R_{1} (x) \in U$
10	3 9	sylib	$⊢ φ \to \forall x \in ω R_{1} (x) \in U$
11	10	r19.21bi	$⊢ (φ \land x \in ω) \to R_{1} (x) \in U$
12		simpr	$⊢ (φ \land x \in ω) \to x \in ω$
13	7 12	sselid	$⊢ (φ \land x \in ω) \to x \in dom R_{1}$
14		onssr1	$⊢ x \in dom R_{1} \to x \subseteq R_{1} (x)$
15	13 14	syl	$⊢ (φ \land x \in ω) \to x \subseteq R_{1} (x)$
16	2 11 15	wunss	$⊢ (φ \land x \in ω) \to x \in U$
17	16	ex	$⊢ φ \to (x \in ω \to x \in U)$
18	17	ssrdv	$⊢ φ \to ω \subseteq U$

Metamath Proof Explorer