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