Step | Hyp | Ref
| Expression |
1 | | frecrdg.1 |
. . . 4
⊢ (φ → 𝐹 Fn V) |
2 | | vex 2554 |
. . . . . 6
⊢ z ∈
V |
3 | | funfvex 5135 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ z ∈ dom 𝐹) → (𝐹‘z) ∈
V) |
4 | 3 | funfni 4942 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ z ∈ V) → (𝐹‘z) ∈
V) |
5 | 2, 4 | mpan2 401 |
. . . . 5
⊢ (𝐹 Fn V → (𝐹‘z) ∈
V) |
6 | 5 | alrimiv 1751 |
. . . 4
⊢ (𝐹 Fn V → ∀z(𝐹‘z) ∈
V) |
7 | 1, 6 | syl 14 |
. . 3
⊢ (φ → ∀z(𝐹‘z) ∈
V) |
8 | | frecrdg.2 |
. . 3
⊢ (φ → A ∈ 𝑉) |
9 | | frecfnom 5925 |
. . 3
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → frec(𝐹, A) Fn
𝜔) |
10 | 7, 8, 9 | syl2anc 391 |
. 2
⊢ (φ → frec(𝐹, A) Fn
𝜔) |
11 | | rdgifnon2 5907 |
. . . 4
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → rec(𝐹, A) Fn
On) |
12 | 7, 8, 11 | syl2anc 391 |
. . 3
⊢ (φ → rec(𝐹, A) Fn
On) |
13 | | omsson 4278 |
. . 3
⊢ 𝜔
⊆ On |
14 | | fnssres 4955 |
. . 3
⊢
((rec(𝐹, A) Fn On ∧
𝜔 ⊆ On) → (rec(𝐹, A)
↾ 𝜔) Fn 𝜔) |
15 | 12, 13, 14 | sylancl 392 |
. 2
⊢ (φ → (rec(𝐹, A)
↾ 𝜔) Fn 𝜔) |
16 | | fveq2 5121 |
. . . . 5
⊢ (x = ∅ → (frec(𝐹, A)‘x) =
(frec(𝐹, A)‘∅)) |
17 | | fveq2 5121 |
. . . . 5
⊢ (x = ∅ → ((rec(𝐹, A)
↾ 𝜔)‘x) = ((rec(𝐹, A) ↾
𝜔)‘∅)) |
18 | 16, 17 | eqeq12d 2051 |
. . . 4
⊢ (x = ∅ → ((frec(𝐹, A)‘x) =
((rec(𝐹, A) ↾ 𝜔)‘x) ↔ (frec(𝐹, A)‘∅) = ((rec(𝐹, A)
↾ 𝜔)‘∅))) |
19 | | fveq2 5121 |
. . . . 5
⊢ (x = y →
(frec(𝐹, A)‘x) =
(frec(𝐹, A)‘y)) |
20 | | fveq2 5121 |
. . . . 5
⊢ (x = y →
((rec(𝐹, A) ↾ 𝜔)‘x) = ((rec(𝐹, A)
↾ 𝜔)‘y)) |
21 | 19, 20 | eqeq12d 2051 |
. . . 4
⊢ (x = y →
((frec(𝐹, A)‘x) =
((rec(𝐹, A) ↾ 𝜔)‘x) ↔ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y))) |
22 | | fveq2 5121 |
. . . . 5
⊢ (x = suc y →
(frec(𝐹, A)‘x) =
(frec(𝐹, A)‘suc y)) |
23 | | fveq2 5121 |
. . . . 5
⊢ (x = suc y →
((rec(𝐹, A) ↾ 𝜔)‘x) = ((rec(𝐹, A)
↾ 𝜔)‘suc y)) |
24 | 22, 23 | eqeq12d 2051 |
. . . 4
⊢ (x = suc y →
((frec(𝐹, A)‘x) =
((rec(𝐹, A) ↾ 𝜔)‘x) ↔ (frec(𝐹, A)‘suc y)
= ((rec(𝐹, A) ↾ 𝜔)‘suc y))) |
25 | | frec0g 5922 |
. . . . . 6
⊢ (A ∈ 𝑉 → (frec(𝐹, A)‘∅) = A) |
26 | 8, 25 | syl 14 |
. . . . 5
⊢ (φ → (frec(𝐹, A)‘∅) = A) |
27 | | peano1 4260 |
. . . . . . 7
⊢ ∅
∈ 𝜔 |
28 | | fvres 5141 |
. . . . . . 7
⊢ (∅
∈ 𝜔 → ((rec(𝐹, A)
↾ 𝜔)‘∅) = (rec(𝐹, A)‘∅)) |
29 | 27, 28 | ax-mp 7 |
. . . . . 6
⊢
((rec(𝐹, A) ↾ 𝜔)‘∅) = (rec(𝐹, A)‘∅) |
30 | | rdg0g 5915 |
. . . . . . 7
⊢ (A ∈ 𝑉 → (rec(𝐹, A)‘∅) = A) |
31 | 8, 30 | syl 14 |
. . . . . 6
⊢ (φ → (rec(𝐹, A)‘∅) = A) |
32 | 29, 31 | syl5eq 2081 |
. . . . 5
⊢ (φ → ((rec(𝐹, A)
↾ 𝜔)‘∅) = A) |
33 | 26, 32 | eqtr4d 2072 |
. . . 4
⊢ (φ → (frec(𝐹, A)‘∅) = ((rec(𝐹, A)
↾ 𝜔)‘∅)) |
34 | | simpr 103 |
. . . . . . . . . 10
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) |
35 | | fvres 5141 |
. . . . . . . . . . 11
⊢ (y ∈ 𝜔
→ ((rec(𝐹, A) ↾ 𝜔)‘y) = (rec(𝐹, A)‘y)) |
36 | 35 | ad2antlr 458 |
. . . . . . . . . 10
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → ((rec(𝐹, A)
↾ 𝜔)‘y) = (rec(𝐹, A)‘y)) |
37 | 34, 36 | eqtrd 2069 |
. . . . . . . . 9
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘y) =
(rec(𝐹, A)‘y)) |
38 | 37 | fveq2d 5125 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (𝐹‘(frec(𝐹, A)‘y)) =
(𝐹‘(rec(𝐹, A)‘y))) |
39 | 7, 8 | jca 290 |
. . . . . . . . . 10
⊢ (φ → (∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉)) |
40 | | frecsuc 5930 |
. . . . . . . . . . 11
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉 ∧ y ∈ 𝜔)
→ (frec(𝐹, A)‘suc y)
= (𝐹‘(frec(𝐹, A)‘y))) |
41 | 40 | 3expa 1103 |
. . . . . . . . . 10
⊢ (((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) ∧
y ∈
𝜔) → (frec(𝐹,
A)‘suc y) = (𝐹‘(frec(𝐹, A)‘y))) |
42 | 39, 41 | sylan 267 |
. . . . . . . . 9
⊢ ((φ ∧ y ∈ 𝜔)
→ (frec(𝐹, A)‘suc y)
= (𝐹‘(frec(𝐹, A)‘y))) |
43 | 42 | adantr 261 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘suc y)
= (𝐹‘(frec(𝐹, A)‘y))) |
44 | 1 | adantr 261 |
. . . . . . . . . 10
⊢ ((φ ∧ y ∈ 𝜔)
→ 𝐹 Fn
V) |
45 | 8 | adantr 261 |
. . . . . . . . . 10
⊢ ((φ ∧ y ∈ 𝜔)
→ A ∈ 𝑉) |
46 | | simpr 103 |
. . . . . . . . . . 11
⊢ ((φ ∧ y ∈ 𝜔)
→ y ∈ 𝜔) |
47 | | nnon 4275 |
. . . . . . . . . . 11
⊢ (y ∈ 𝜔
→ y ∈ On) |
48 | 46, 47 | syl 14 |
. . . . . . . . . 10
⊢ ((φ ∧ y ∈ 𝜔)
→ y ∈ On) |
49 | | frecrdg.inc |
. . . . . . . . . . 11
⊢ (φ → ∀x x ⊆ (𝐹‘x)) |
50 | 49 | adantr 261 |
. . . . . . . . . 10
⊢ ((φ ∧ y ∈ 𝜔)
→ ∀x x ⊆
(𝐹‘x)) |
51 | 44, 45, 48, 50 | rdgisucinc 5912 |
. . . . . . . . 9
⊢ ((φ ∧ y ∈ 𝜔)
→ (rec(𝐹, A)‘suc y)
= (𝐹‘(rec(𝐹, A)‘y))) |
52 | 51 | adantr 261 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (rec(𝐹, A)‘suc y)
= (𝐹‘(rec(𝐹, A)‘y))) |
53 | 38, 43, 52 | 3eqtr4d 2079 |
. . . . . . 7
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘suc y)
= (rec(𝐹, A)‘suc y)) |
54 | | peano2 4261 |
. . . . . . . . 9
⊢ (y ∈ 𝜔
→ suc y ∈ 𝜔) |
55 | | fvres 5141 |
. . . . . . . . 9
⊢ (suc
y ∈
𝜔 → ((rec(𝐹,
A) ↾ 𝜔)‘suc y) = (rec(𝐹, A)‘suc y)) |
56 | 54, 55 | syl 14 |
. . . . . . . 8
⊢ (y ∈ 𝜔
→ ((rec(𝐹, A) ↾ 𝜔)‘suc y) = (rec(𝐹, A)‘suc y)) |
57 | 56 | ad2antlr 458 |
. . . . . . 7
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → ((rec(𝐹, A)
↾ 𝜔)‘suc y) =
(rec(𝐹, A)‘suc y)) |
58 | 53, 57 | eqtr4d 2072 |
. . . . . 6
⊢ (((φ ∧ y ∈ 𝜔)
∧ (frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘suc y)
= ((rec(𝐹, A) ↾ 𝜔)‘suc y)) |
59 | 58 | ex 108 |
. . . . 5
⊢ ((φ ∧ y ∈ 𝜔)
→ ((frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y) → (frec(𝐹, A)‘suc y)
= ((rec(𝐹, A) ↾ 𝜔)‘suc y))) |
60 | 59 | expcom 109 |
. . . 4
⊢ (y ∈ 𝜔
→ (φ → ((frec(𝐹, A)‘y) =
((rec(𝐹, A) ↾ 𝜔)‘y) → (frec(𝐹, A)‘suc y)
= ((rec(𝐹, A) ↾ 𝜔)‘suc y)))) |
61 | 18, 21, 24, 33, 60 | finds2 4267 |
. . 3
⊢ (x ∈ 𝜔
→ (φ → (frec(𝐹, A)‘x) =
((rec(𝐹, A) ↾ 𝜔)‘x))) |
62 | 61 | impcom 116 |
. 2
⊢ ((φ ∧ x ∈ 𝜔)
→ (frec(𝐹, A)‘x) =
((rec(𝐹, A) ↾ 𝜔)‘x)) |
63 | 10, 15, 62 | eqfnfvd 5211 |
1
⊢ (φ → frec(𝐹, A) =
(rec(𝐹, A) ↾ 𝜔)) |