Metamath Proof Explorer

Theorem tskr1om

Description: A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by Mario Carneiro, 24-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
2 1 eleq1d 
 |-  ( x = (/) -> ( ( R1 ` x ) e. T <-> ( R1 ` (/) ) e. T ) )
3 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
4 3 eleq1d 
 |-  ( x = y -> ( ( R1 ` x ) e. T <-> ( R1 ` y ) e. T ) )
5 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
6 5 eleq1d 
 |-  ( x = suc y -> ( ( R1 ` x ) e. T <-> ( R1 ` suc y ) e. T ) )
7 r10 
 |-  ( R1 ` (/) ) = (/)
8 tsk0 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> (/) e. T )
9 7 8 eqeltrid 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 ` (/) ) e. T )
10 tskpw 
 |-  ( ( T e. Tarski /\ ( R1 ` y ) e. T ) -> ~P ( R1 ` y ) e. T )
11 nnon 
 |-  ( y e. _om -> y e. On )
12 r1suc 
 |-  ( y e. On -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
13 11 12 syl 
 |-  ( y e. _om -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
14 13 eleq1d 
 |-  ( y e. _om -> ( ( R1 ` suc y ) e. T <-> ~P ( R1 ` y ) e. T ) )
15 10 14 imbitrrid 
 |-  ( y e. _om -> ( ( T e. Tarski /\ ( R1 ` y ) e. T ) -> ( R1 ` suc y ) e. T ) )
16 15 expd 
 |-  ( y e. _om -> ( T e. Tarski -> ( ( R1 ` y ) e. T -> ( R1 ` suc y ) e. T ) ) )
17 16 adantrd 
 |-  ( y e. _om -> ( ( T e. Tarski /\ T =/= (/) ) -> ( ( R1 ` y ) e. T -> ( R1 ` suc y ) e. T ) ) )
18 2 4 6 9 17 finds2 
 |-  ( x e. _om -> ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 ` x ) e. T ) )
19 eleq1 
 |-  ( ( R1 ` x ) = y -> ( ( R1 ` x ) e. T <-> y e. T ) )
20 19 imbi2d 
 |-  ( ( R1 ` x ) = y -> ( ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 ` x ) e. T ) <-> ( ( T e. Tarski /\ T =/= (/) ) -> y e. T ) ) )
21 18 20 syl5ibcom 
 |-  ( x e. _om -> ( ( R1 ` x ) = y -> ( ( T e. Tarski /\ T =/= (/) ) -> y e. T ) ) )
22 21 rexlimiv 
 |-  ( E. x e. _om ( R1 ` x ) = y -> ( ( T e. Tarski /\ T =/= (/) ) -> y e. T ) )
23 r1fnon 
 |-  R1 Fn On
24 fnfun 
 |-  ( R1 Fn On -> Fun R1 )
25 23 24 ax-mp 
 |-  Fun R1
26 fvelima 
 |-  ( ( Fun R1 /\ y e. ( R1 " _om ) ) -> E. x e. _om ( R1 ` x ) = y )
27 25 26 mpan 
 |-  ( y e. ( R1 " _om ) -> E. x e. _om ( R1 ` x ) = y )
28 22 27 syl11 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( y e. ( R1 " _om ) -> y e. T ) )
29 28 ssrdv 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) C_ T )