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		r1fun	|- Fun R1
5		r1dmlim	|- Lim dom R1
6		limomss	|- ( Lim dom R1 -> _om C_ dom R1 )
7	5 6	ax-mp	|- _om C_ dom R1
8		funimass4	|- ( ( Fun R1 /\ _om C_ dom R1 ) -> ( ( R1 " _om ) C_ U <-> A. x e. _om ( R1 ` x ) e. U ) )
9	4 7 8	mp2an	|- ( ( R1 " _om ) C_ U <-> A. x e. _om ( R1 ` x ) e. U )
10	3 9	sylib	|- ( ph -> A. x e. _om ( R1 ` x ) e. U )
11	10	r19.21bi	|- ( ( ph /\ x e. _om ) -> ( R1 ` x ) e. U )
12		simpr	|- ( ( ph /\ x e. _om ) -> x e. _om )
13	7 12	sselid	|- ( ( ph /\ x e. _om ) -> x e. dom R1 )
14		onssr1	|- ( x e. dom R1 -> x C_ ( R1 ` x ) )
15	13 14	syl	|- ( ( ph /\ x e. _om ) -> x C_ ( R1 ` x ) )
16	2 11 15	wunss	|- ( ( ph /\ x e. _om ) -> x e. U )
17	16	ex	|- ( ph -> ( x e. _om -> x e. U ) )
18	17	ssrdv	|- ( ph -> _om C_ U )