| Step | Hyp | Ref
| Expression |
| 1 | | noseq.1 |
. . 3
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “
ω)) |
| 2 | | df-ima 5698 |
. . 3
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
“ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω) |
| 3 | 1, 2 | eqtrdi 2793 |
. 2
⊢ (𝜑 → 𝑍 = ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)) |
| 4 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = ∅ → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑧) =
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘∅)) |
| 5 | 4 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑧 = ∅ → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑧) ∈
𝐵 ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘∅) ∈ 𝐵)) |
| 6 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤)) |
| 7 | 6 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) ∈ 𝐵 ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) ∈ 𝐵)) |
| 8 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = suc 𝑤 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘suc
𝑤)) |
| 9 | 8 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑧 = suc 𝑤 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) ∈ 𝐵 ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘suc
𝑤) ∈ 𝐵)) |
| 10 | | noseq.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ No
) |
| 11 | | fr0g 8476 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → ((rec((𝑥
∈ V ↦ (𝑥
+s 1s )), 𝐴) ↾ ω)‘∅) = 𝐴) |
| 12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)‘∅) = 𝐴) |
| 13 | | noseqind.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 14 | 12, 13 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω)‘∅) ∈ 𝐵) |
| 15 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) → (𝑦 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑤)
+s 1s )) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) → ((𝑦 +s 1s ) ∈ 𝐵 ↔ (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑤)
+s 1s ) ∈ 𝐵)) |
| 17 | 16 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑦 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) → ((𝜑 → (𝑦 +s 1s ) ∈ 𝐵) ↔ (𝜑 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) +s 1s )
∈ 𝐵))) |
| 18 | | noseqind.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵) |
| 19 | 18 | expcom 413 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 → (𝜑 → (𝑦 +s 1s ) ∈ 𝐵)) |
| 20 | 17, 19 | vtoclga 3577 |
. . . . . . . . . 10
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑤)
∈ 𝐵 → (𝜑 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) +s 1s )
∈ 𝐵)) |
| 21 | 20 | impcom 407 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) ∈ 𝐵) → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) +s 1s )
∈ 𝐵) |
| 22 | | ovex 7464 |
. . . . . . . . . . 11
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑤)
+s 1s ) ∈ V |
| 23 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥
+s 1s )), 𝐴) ↾ ω) |
| 24 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → (𝑡 +s 1s ) = (𝑥 +s 1s
)) |
| 25 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑡 = ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) → (𝑡 +s 1s ) =
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑤)
+s 1s )) |
| 26 | 23, 24, 25 | frsucmpt2 8480 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ω ∧
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑤)
+s 1s ) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘suc
𝑤) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑤)
+s 1s )) |
| 27 | 22, 26 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ω →
((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘suc 𝑤) = (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) +s 1s
)) |
| 28 | 27 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑤 ∈ ω →
(((rec((𝑥 ∈ V ↦
(𝑥 +s
1s )), 𝐴)
↾ ω)‘suc 𝑤) ∈ 𝐵 ↔ (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) +s 1s )
∈ 𝐵)) |
| 29 | 21, 28 | imbitrrid 246 |
. . . . . . . 8
⊢ (𝑤 ∈ ω → ((𝜑 ∧ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) ∈ 𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘suc
𝑤) ∈ 𝐵)) |
| 30 | 29 | expd 415 |
. . . . . . 7
⊢ (𝑤 ∈ ω → (𝜑 → (((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑤) ∈ 𝐵 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘suc
𝑤) ∈ 𝐵))) |
| 31 | 5, 7, 9, 14, 30 | finds2 7920 |
. . . . . 6
⊢ (𝑧 ∈ ω → (𝜑 → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) ∈ 𝐵)) |
| 32 | 31 | com12 32 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾
ω)‘𝑧) ∈
𝐵)) |
| 33 | 32 | ralrimiv 3145 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) ∈ 𝐵) |
| 34 | | frfnom 8475 |
. . . . 5
⊢
(rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω) Fn ω |
| 35 | | ffnfv 7139 |
. . . . 5
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω):ω⟶𝐵 ↔ ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω) Fn ω
∧ ∀𝑧 ∈
ω ((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω)‘𝑧)
∈ 𝐵)) |
| 36 | 34, 35 | mpbiran 709 |
. . . 4
⊢
((rec((𝑥 ∈ V
↦ (𝑥 +s
1s )), 𝐴)
↾ ω):ω⟶𝐵 ↔ ∀𝑧 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾ ω)‘𝑧) ∈ 𝐵) |
| 37 | 33, 36 | sylibr 234 |
. . 3
⊢ (𝜑 → (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) ↾
ω):ω⟶𝐵) |
| 38 | 37 | frnd 6744 |
. 2
⊢ (𝜑 → ran (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
𝐴) ↾ ω) ⊆
𝐵) |
| 39 | 3, 38 | eqsstrd 4018 |
1
⊢ (𝜑 → 𝑍 ⊆ 𝐵) |