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 syl5ibr
 |-  ( 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 )