Step | Hyp | Ref
| Expression |
1 | | r1fnon 8513 |
. . . . . 6
⊢
𝑅1 Fn On |
2 | | fnfun 5902 |
. . . . . 6
⊢
(𝑅1 Fn On → Fun
𝑅1) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ Fun
𝑅1 |
4 | | fvelima 6158 |
. . . . 5
⊢ ((Fun
𝑅1 ∧ 𝑦 ∈ (𝑅1 “
ω)) → ∃𝑥
∈ ω (𝑅1‘𝑥) = 𝑦) |
5 | 3, 4 | mpan 702 |
. . . 4
⊢ (𝑦 ∈ (𝑅1
“ ω) → ∃𝑥 ∈ ω
(𝑅1‘𝑥) = 𝑦) |
6 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) |
7 | 6 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = ∅ →
((𝑅1‘𝑥) ∈ 𝑇 ↔
(𝑅1‘∅) ∈ 𝑇)) |
8 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
9 | 8 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ∈ 𝑇 ↔ (𝑅1‘𝑦) ∈ 𝑇)) |
10 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
11 | 10 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ∈ 𝑇 ↔ (𝑅1‘suc
𝑦) ∈ 𝑇)) |
12 | | r10 8514 |
. . . . . . . 8
⊢
(𝑅1‘∅) = ∅ |
13 | | tsk0 9464 |
. . . . . . . 8
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅
∈ 𝑇) |
14 | 12, 13 | syl5eqel 2692 |
. . . . . . 7
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(𝑅1‘∅) ∈ 𝑇) |
15 | | tskpw 9454 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧
(𝑅1‘𝑦) ∈ 𝑇) → 𝒫
(𝑅1‘𝑦) ∈ 𝑇) |
16 | | nnon 6963 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
17 | | r1suc 8516 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) |
19 | 18 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω →
((𝑅1‘suc 𝑦) ∈ 𝑇 ↔ 𝒫
(𝑅1‘𝑦) ∈ 𝑇)) |
20 | 15, 19 | syl5ibr 235 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → ((𝑇 ∈ Tarski ∧
(𝑅1‘𝑦) ∈ 𝑇) → (𝑅1‘suc
𝑦) ∈ 𝑇)) |
21 | 20 | expd 451 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (𝑇 ∈ Tarski →
((𝑅1‘𝑦) ∈ 𝑇 → (𝑅1‘suc
𝑦) ∈ 𝑇))) |
22 | 21 | adantrd 483 |
. . . . . . 7
⊢ (𝑦 ∈ ω → ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
((𝑅1‘𝑦) ∈ 𝑇 → (𝑅1‘suc
𝑦) ∈ 𝑇))) |
23 | 7, 9, 11, 14, 22 | finds2 6986 |
. . . . . 6
⊢ (𝑥 ∈ ω → ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(𝑅1‘𝑥) ∈ 𝑇)) |
24 | | eleq1 2676 |
. . . . . . 7
⊢
((𝑅1‘𝑥) = 𝑦 → ((𝑅1‘𝑥) ∈ 𝑇 ↔ 𝑦 ∈ 𝑇)) |
25 | 24 | imbi2d 329 |
. . . . . 6
⊢
((𝑅1‘𝑥) = 𝑦 → (((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(𝑅1‘𝑥) ∈ 𝑇) ↔ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 𝑦 ∈ 𝑇))) |
26 | 23, 25 | syl5ibcom 234 |
. . . . 5
⊢ (𝑥 ∈ ω →
((𝑅1‘𝑥) = 𝑦 → ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 𝑦 ∈ 𝑇))) |
27 | 26 | rexlimiv 3009 |
. . . 4
⊢
(∃𝑥 ∈
ω (𝑅1‘𝑥) = 𝑦 → ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 𝑦 ∈ 𝑇)) |
28 | 5, 27 | syl 17 |
. . 3
⊢ (𝑦 ∈ (𝑅1
“ ω) → ((𝑇
∈ Tarski ∧ 𝑇 ≠
∅) → 𝑦 ∈
𝑇)) |
29 | 28 | com12 32 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑦 ∈ (𝑅1
“ ω) → 𝑦
∈ 𝑇)) |
30 | 29 | ssrdv 3574 |
1
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(𝑅1 “ ω) ⊆ 𝑇) |