Step | Hyp | Ref
| Expression |
1 | | eqid 2037 |
. . . 4
⊢
recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))})) =
recs((g ∈
V ↦ {x ∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))})) |
2 | | eqid 2037 |
. . . . 5
⊢ (g ∈ V ↦
{x ∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}) =
(g ∈ V
↦ {x ∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}) |
3 | 2 | frectfr 5924 |
. . . 4
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → ∀y(Fun
(g ∈ V
↦ {x ∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}) ∧ ((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))})‘y)
∈ V)) |
4 | 1, 3 | tfri1d 5890 |
. . 3
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → recs((g ∈ V ↦
{x ∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))})) Fn
On) |
5 | | fnresin1 4956 |
. . 3
⊢
(recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))})) Fn On
→ (recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) Fn (On ∩ 𝜔)) |
6 | 4, 5 | syl 14 |
. 2
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → (recs((g ∈ V ↦
{x ∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) Fn (On ∩ 𝜔)) |
7 | | omsson 4278 |
. . . . . 6
⊢ 𝜔
⊆ On |
8 | | sseqin2 3150 |
. . . . . 6
⊢
(𝜔 ⊆ On ↔ (On ∩ 𝜔) =
𝜔) |
9 | 7, 8 | mpbi 133 |
. . . . 5
⊢ (On ∩
𝜔) = 𝜔 |
10 | 9 | reseq2i 4552 |
. . . 4
⊢
(recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) = (recs((g
∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ 𝜔) |
11 | | df-frec 5918 |
. . . 4
⊢
frec(𝐹, A) = (recs((g
∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ 𝜔) |
12 | 10, 11 | eqtr4i 2060 |
. . 3
⊢
(recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) = frec(𝐹, A) |
13 | | fneq12 4935 |
. . 3
⊢
(((recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) = frec(𝐹, A)
∧ (On ∩ 𝜔) = 𝜔) →
((recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) Fn (On ∩ 𝜔) ↔ frec(𝐹, A) Fn 𝜔)) |
14 | 12, 9, 13 | mp2an 402 |
. 2
⊢
((recs((g ∈ V ↦ {x
∣ (∃𝑚 ∈
𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom
g = ∅ ∧ x ∈ A))}))
↾ (On ∩ 𝜔)) Fn (On ∩ 𝜔) ↔ frec(𝐹, A) Fn 𝜔) |
15 | 6, 14 | sylib 127 |
1
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → frec(𝐹, A) Fn
𝜔) |