Theorem tskr1om2

Description: A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by NM, 22-Feb-2011)

	Ref	Expression
Assertion	tskr1om2	|- ( ( T e. Tarski /\ T =/= (/) ) -> U. ( R1 " _om ) C_ T )

Proof

Step	Hyp	Ref	Expression
1		eluni2	|- ( y e. U. ( R1 " _om ) <-> E. x e. ( R1 " _om ) y e. x )
2		r1fnon	|- R1 Fn On
3		fnfun	|- ( R1 Fn On -> Fun R1 )
4	2 3	ax-mp	|- Fun R1
5		fvelima	|- ( ( Fun R1 /\ x e. ( R1 " _om ) ) -> E. y e. _om ( R1 ` y ) = x )
6	4 5	mpan	|- ( x e. ( R1 " _om ) -> E. y e. _om ( R1 ` y ) = x )
7		r1tr	|- Tr ( R1 ` y )
8		treq	|- ( ( R1 ` y ) = x -> ( Tr ( R1 ` y ) <-> Tr x ) )
9	7 8	mpbii	|- ( ( R1 ` y ) = x -> Tr x )
10	9	rexlimivw	|- ( E. y e. _om ( R1 ` y ) = x -> Tr x )
11		trss	|- ( Tr x -> ( y e. x -> y C_ x ) )
12	6 10 11	3syl	|- ( x e. ( R1 " _om ) -> ( y e. x -> y C_ x ) )
13	12	adantl	|- ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y e. x -> y C_ x ) )
14		tskr1om	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) C_ T )
15	14	sseld	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. ( R1 " _om ) -> x e. T ) )
16		tskss	|- ( ( T e. Tarski /\ x e. T /\ y C_ x ) -> y e. T )
17	16	3exp	|- ( T e. Tarski -> ( x e. T -> ( y C_ x -> y e. T ) ) )
18	17	adantr	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. T -> ( y C_ x -> y e. T ) ) )
19	15 18	syld	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. ( R1 " _om ) -> ( y C_ x -> y e. T ) ) )
20	19	imp	|- ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y C_ x -> y e. T ) )
21	13 20	syld	|- ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y e. x -> y e. T ) )
22	21	rexlimdva	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( E. x e. ( R1 " _om ) y e. x -> y e. T ) )
23	1 22	biimtrid	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( y e. U. ( R1 " _om ) -> y e. T ) )
24	23	ssrdv	|- ( ( T e. Tarski /\ T =/= (/) ) -> U. ( R1 " _om ) C_ T )