| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | noseqp1.3 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑍) | 
| 2 |  | noseq.1 | . . . . 5
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “
ω)) | 
| 3 | 1, 2 | eleqtrd 2842 | . . . 4
⊢ (𝜑 → 𝐵 ∈ (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “
ω)) | 
| 4 |  | df-ima 5697 | . . . 4
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
“ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω) | 
| 5 | 3, 4 | eleqtrdi 2850 | . . 3
⊢ (𝜑 → 𝐵 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)) | 
| 6 |  | frfnom 8476 | . . . 4
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω) Fn ω | 
| 7 |  | fvelrnb 6968 | . . . 4
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω) Fn ω → (𝐵 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦) =
𝐵)) | 
| 8 | 6, 7 | ax-mp 5 | . . 3
⊢ (𝐵 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾ ω) ↔
∃𝑦 ∈ ω
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦) =
𝐵) | 
| 9 | 5, 8 | sylib 218 | . 2
⊢ (𝜑 → ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑦) = 𝐵) | 
| 10 |  | ovex 7465 | . . . . . . 7
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦)
+s 1s ) ∈ V | 
| 11 |  | eqid 2736 | . . . . . . . 8
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥
+s 1s )), 𝐴) ↾ ω) | 
| 12 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 +s 1s ) = (𝑥 +s 1s
)) | 
| 13 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑦) → (𝑧 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦)
+s 1s )) | 
| 14 | 11, 12, 13 | frsucmpt2 8481 | . . . . . . 7
⊢ ((𝑦 ∈ ω ∧
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦)
+s 1s ) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘suc
𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑦)
+s 1s )) | 
| 15 | 10, 14 | mpan2 691 | . . . . . 6
⊢ (𝑦 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑦) +s 1s
)) | 
| 16 | 15 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘suc 𝑦) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦)
+s 1s )) | 
| 17 |  | peano2 7913 | . . . . . . . 8
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) | 
| 18 |  | fnfvelrn 7099 | . . . . . . . 8
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘suc 𝑦)
∈ ran (rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)) | 
| 19 | 6, 17, 18 | sylancr 587 | . . . . . . 7
⊢ (𝑦 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)) | 
| 20 | 19 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘suc 𝑦)
∈ ran (rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)) | 
| 21 | 2, 4 | eqtrdi 2792 | . . . . . . 7
⊢ (𝜑 → 𝑍 = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)) | 
| 22 | 21 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑍 = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)) | 
| 23 | 20, 22 | eleqtrrd 2843 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘suc 𝑦)
∈ 𝑍) | 
| 24 | 16, 23 | eqeltrrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑦)
+s 1s ) ∈ 𝑍) | 
| 25 |  | oveq1 7439 | . . . . 5
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦) =
𝐵 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑦)
+s 1s ) = (𝐵 +s 1s
)) | 
| 26 | 25 | eleq1d 2825 | . . . 4
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑦) =
𝐵 → ((((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑦)
+s 1s ) ∈ 𝑍 ↔ (𝐵 +s 1s ) ∈ 𝑍)) | 
| 27 | 24, 26 | syl5ibcom 245 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑦) = 𝐵 → (𝐵 +s 1s ) ∈ 𝑍)) | 
| 28 | 27 | impr 454 | . 2
⊢ ((𝜑 ∧ (𝑦 ∈ ω ∧ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑦) = 𝐵)) → (𝐵 +s 1s ) ∈ 𝑍) | 
| 29 | 9, 28 | rexlimddv 3160 | 1
⊢ (𝜑 → (𝐵 +s 1s ) ∈ 𝑍) |