This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )