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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
5	4	simpli	$⊢ Fun R_{1}$
6	4	simpri	$⊢ Lim dom R_{1}$
7		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
8	6 7	ax-mp	$⊢ ω \subseteq dom R_{1}$
9		funimass4	$⊢ (Fun R_{1} \land ω \subseteq dom R_{1}) \to (R_{1} [ω] \subseteq U \leftrightarrow \forall x \in ω R_{1} (x) \in U)$
10	5 8 9	mp2an	$⊢ R_{1} [ω] \subseteq U \leftrightarrow \forall x \in ω R_{1} (x) \in U$
11	3 10	sylib	$⊢ φ \to \forall x \in ω R_{1} (x) \in U$
12	11	r19.21bi	$⊢ (φ \land x \in ω) \to R_{1} (x) \in U$
13		simpr	$⊢ (φ \land x \in ω) \to x \in ω$
14	8 13	sseldi	$⊢ (φ \land x \in ω) \to x \in dom R_{1}$
15		onssr1	$⊢ x \in dom R_{1} \to x \subseteq R_{1} (x)$
16	14 15	syl	$⊢ (φ \land x \in ω) \to x \subseteq R_{1} (x)$
17	2 12 16	wunss	$⊢ (φ \land x \in ω) \to x \in U$
18	17	ex	$⊢ φ \to (x \in ω \to x \in U)$
19	18	ssrdv	$⊢ φ \to ω \subseteq U$

Metamath Proof Explorer