Step | Hyp | Ref
| Expression |
1 | | frecrdg.1 |
. . . 4
⊢ (𝜑 → 𝐹 Fn V) |
2 | | vex 2560 |
. . . . . 6
⊢ 𝑧 ∈ V |
3 | | funfvex 5192 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ V) |
4 | 3 | funfni 4999 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ V) |
5 | 2, 4 | mpan2 401 |
. . . . 5
⊢ (𝐹 Fn V → (𝐹‘𝑧) ∈ V) |
6 | 5 | alrimiv 1754 |
. . . 4
⊢ (𝐹 Fn V → ∀𝑧(𝐹‘𝑧) ∈ V) |
7 | 1, 6 | syl 14 |
. . 3
⊢ (𝜑 → ∀𝑧(𝐹‘𝑧) ∈ V) |
8 | | frecrdg.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
9 | | frecfnom 5986 |
. . 3
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → frec(𝐹, 𝐴) Fn ω) |
10 | 7, 8, 9 | syl2anc 391 |
. 2
⊢ (𝜑 → frec(𝐹, 𝐴) Fn ω) |
11 | | rdgifnon2 5967 |
. . . 4
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On) |
12 | 7, 8, 11 | syl2anc 391 |
. . 3
⊢ (𝜑 → rec(𝐹, 𝐴) Fn On) |
13 | | omsson 4335 |
. . 3
⊢ ω
⊆ On |
14 | | fnssres 5012 |
. . 3
⊢
((rec(𝐹, 𝐴) Fn On ∧ ω ⊆
On) → (rec(𝐹, 𝐴) ↾ ω) Fn
ω) |
15 | 12, 13, 14 | sylancl 392 |
. 2
⊢ (𝜑 → (rec(𝐹, 𝐴) ↾ ω) Fn
ω) |
16 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = ∅ → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘∅)) |
17 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾
ω)‘∅)) |
18 | 16, 17 | eqeq12d 2054 |
. . . 4
⊢ (𝑥 = ∅ → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾
ω)‘∅))) |
19 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘𝑦)) |
20 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) |
21 | 19, 20 | eqeq12d 2054 |
. . . 4
⊢ (𝑥 = 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦))) |
22 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘suc 𝑦)) |
23 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)) |
24 | 22, 23 | eqeq12d 2054 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))) |
25 | | frec0g 5983 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴) |
26 | 8, 25 | syl 14 |
. . . . 5
⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = 𝐴) |
27 | | peano1 4317 |
. . . . . . 7
⊢ ∅
∈ ω |
28 | | fvres 5198 |
. . . . . . 7
⊢ (∅
∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘∅) =
(rec(𝐹, 𝐴)‘∅)) |
29 | 27, 28 | ax-mp 7 |
. . . . . 6
⊢
((rec(𝐹, 𝐴) ↾
ω)‘∅) = (rec(𝐹, 𝐴)‘∅) |
30 | | rdg0g 5975 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴) |
31 | 8, 30 | syl 14 |
. . . . . 6
⊢ (𝜑 → (rec(𝐹, 𝐴)‘∅) = 𝐴) |
32 | 29, 31 | syl5eq 2084 |
. . . . 5
⊢ (𝜑 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴) |
33 | 26, 32 | eqtr4d 2075 |
. . . 4
⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾
ω)‘∅)) |
34 | | simpr 103 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) |
35 | | fvres 5198 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω →
((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦)) |
36 | 35 | ad2antlr 458 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦)) |
37 | 34, 36 | eqtrd 2072 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦)) |
38 | 37 | fveq2d 5182 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦))) |
39 | 7, 8 | jca 290 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉)) |
40 | | frecsuc 5991 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
41 | 40 | 3expa 1104 |
. . . . . . . . . 10
⊢
(((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
42 | 39, 41 | sylan 267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
43 | 42 | adantr 261 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
44 | 1 | adantr 261 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐹 Fn V) |
45 | 8 | adantr 261 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝑉) |
46 | | simpr 103 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ ω) |
47 | | nnon 4332 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
48 | 46, 47 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ On) |
49 | | frecrdg.inc |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) |
50 | 49 | adantr 261 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) |
51 | 44, 45, 48, 50 | rdgisucinc 5972 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦))) |
52 | 51 | adantr 261 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦))) |
53 | 38, 43, 52 | 3eqtr4d 2082 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
54 | | peano2 4318 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
55 | | fvres 5198 |
. . . . . . . . 9
⊢ (suc
𝑦 ∈ ω →
((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
56 | 54, 55 | syl 14 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
57 | 56 | ad2antlr 458 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
58 | 53, 57 | eqtr4d 2075 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)) |
59 | 58 | ex 108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))) |
60 | 59 | expcom 109 |
. . . 4
⊢ (𝑦 ∈ ω → (𝜑 → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)))) |
61 | 18, 21, 24, 33, 60 | finds2 4324 |
. . 3
⊢ (𝑥 ∈ ω → (𝜑 → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥))) |
62 | 61 | impcom 116 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥)) |
63 | 10, 15, 62 | eqfnfvd 5268 |
1
⊢ (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω)) |