Theorem 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	|- ( ph -> U e. WUni )
Assertion	wunom	|- ( ph -> _om C_ U )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	|- ( ph -> U e. WUni )
2	1	adantr	|- ( ( ph /\ x e. _om ) -> U e. WUni )
3	1	wunr1om	|- ( ph -> ( R1 " _om ) C_ U )
4		r1funlim	|- ( Fun R1 /\ Lim dom R1 )
5	4	simpli	|- Fun R1
6	4	simpri	|- Lim dom R1
7		limomss	|- ( Lim dom R1 -> _om C_ dom R1 )
8	6 7	ax-mp	|- _om C_ dom R1
9		funimass4	|- ( ( Fun R1 /\ _om C_ dom R1 ) -> ( ( R1 " _om ) C_ U <-> A. x e. _om ( R1 ` x ) e. U ) )
10	5 8 9	mp2an	|- ( ( R1 " _om ) C_ U <-> A. x e. _om ( R1 ` x ) e. U )
11	3 10	sylib	|- ( ph -> A. x e. _om ( R1 ` x ) e. U )
12	11	r19.21bi	|- ( ( ph /\ x e. _om ) -> ( R1 ` x ) e. U )
13		simpr	|- ( ( ph /\ x e. _om ) -> x e. _om )
14	8 13	sselid	|- ( ( ph /\ x e. _om ) -> x e. dom R1 )
15		onssr1	|- ( x e. dom R1 -> x C_ ( R1 ` x ) )
16	14 15	syl	|- ( ( ph /\ x e. _om ) -> x C_ ( R1 ` x ) )
17	2 12 16	wunss	|- ( ( ph /\ x e. _om ) -> x e. U )
18	17	ex	|- ( ph -> ( x e. _om -> x e. U ) )
19	18	ssrdv	|- ( ph -> _om C_ U )