Step | Hyp | Ref
| Expression |
1 | | frecrdg.1 |
. . . 4
⊢ (𝜑 → 𝐹 Fn V) |
2 | | vex 2733 |
. . . . . 6
⊢ 𝑧 ∈ V |
3 | | funfvex 5511 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ V) |
4 | 3 | funfni 5296 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ V) |
5 | 2, 4 | mpan2 423 |
. . . . 5
⊢ (𝐹 Fn V → (𝐹‘𝑧) ∈ V) |
6 | 5 | alrimiv 1867 |
. . . 4
⊢ (𝐹 Fn V → ∀𝑧(𝐹‘𝑧) ∈ V) |
7 | 1, 6 | syl 14 |
. . 3
⊢ (𝜑 → ∀𝑧(𝐹‘𝑧) ∈ V) |
8 | | frecrdg.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
9 | | frecfnom 6378 |
. . 3
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → frec(𝐹, 𝐴) Fn ω) |
10 | 7, 8, 9 | syl2anc 409 |
. 2
⊢ (𝜑 → frec(𝐹, 𝐴) Fn ω) |
11 | | rdgifnon2 6357 |
. . . 4
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On) |
12 | 7, 8, 11 | syl2anc 409 |
. . 3
⊢ (𝜑 → rec(𝐹, 𝐴) Fn On) |
13 | | omsson 4595 |
. . 3
⊢ ω
⊆ On |
14 | | fnssres 5309 |
. . 3
⊢
((rec(𝐹, 𝐴) Fn On ∧ ω ⊆
On) → (rec(𝐹, 𝐴) ↾ ω) Fn
ω) |
15 | 12, 13, 14 | sylancl 411 |
. 2
⊢ (𝜑 → (rec(𝐹, 𝐴) ↾ ω) Fn
ω) |
16 | | fveq2 5494 |
. . . . 5
⊢ (𝑥 = ∅ → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘∅)) |
17 | | fveq2 5494 |
. . . . 5
⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾
ω)‘∅)) |
18 | 16, 17 | eqeq12d 2185 |
. . . 4
⊢ (𝑥 = ∅ → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾
ω)‘∅))) |
19 | | fveq2 5494 |
. . . . 5
⊢ (𝑥 = 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘𝑦)) |
20 | | fveq2 5494 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) |
21 | 19, 20 | eqeq12d 2185 |
. . . 4
⊢ (𝑥 = 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦))) |
22 | | fveq2 5494 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘suc 𝑦)) |
23 | | fveq2 5494 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)) |
24 | 22, 23 | eqeq12d 2185 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))) |
25 | | frec0g 6374 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴) |
26 | 8, 25 | syl 14 |
. . . . 5
⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = 𝐴) |
27 | | peano1 4576 |
. . . . . . 7
⊢ ∅
∈ ω |
28 | | fvres 5518 |
. . . . . . 7
⊢ (∅
∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘∅) =
(rec(𝐹, 𝐴)‘∅)) |
29 | 27, 28 | ax-mp 5 |
. . . . . 6
⊢
((rec(𝐹, 𝐴) ↾
ω)‘∅) = (rec(𝐹, 𝐴)‘∅) |
30 | | rdg0g 6365 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴) |
31 | 8, 30 | syl 14 |
. . . . . 6
⊢ (𝜑 → (rec(𝐹, 𝐴)‘∅) = 𝐴) |
32 | 29, 31 | eqtrid 2215 |
. . . . 5
⊢ (𝜑 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴) |
33 | 26, 32 | eqtr4d 2206 |
. . . 4
⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾
ω)‘∅)) |
34 | | simpr 109 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) |
35 | | fvres 5518 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω →
((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦)) |
36 | 35 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦)) |
37 | 34, 36 | eqtrd 2203 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦)) |
38 | 37 | fveq2d 5498 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦))) |
39 | 7, 8 | jca 304 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉)) |
40 | | simp1 992 |
. . . . . . . . . . . . 13
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → ∀𝑧(𝐹‘𝑧) ∈ V) |
41 | | ralv 2747 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈ V
(𝐹‘𝑧) ∈ V ↔ ∀𝑧(𝐹‘𝑧) ∈ V) |
42 | 40, 41 | sylibr 133 |
. . . . . . . . . . . 12
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → ∀𝑧 ∈ V (𝐹‘𝑧) ∈ V) |
43 | | simp2 993 |
. . . . . . . . . . . . 13
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝑉) |
44 | 43 | elexd 2743 |
. . . . . . . . . . . 12
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → 𝐴 ∈ V) |
45 | | simp3 994 |
. . . . . . . . . . . 12
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → 𝑦 ∈ ω) |
46 | | frecsuc 6384 |
. . . . . . . . . . . 12
⊢
((∀𝑧 ∈ V
(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ V ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
47 | 42, 44, 45, 46 | syl3anc 1233 |
. . . . . . . . . . 11
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
48 | 47 | 3expa 1198 |
. . . . . . . . . 10
⊢
(((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
49 | 39, 48 | sylan 281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
50 | 49 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
51 | 1 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐹 Fn V) |
52 | 8 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝑉) |
53 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ ω) |
54 | | nnon 4592 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
55 | 53, 54 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ On) |
56 | | frecrdg.inc |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) |
57 | 56 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) |
58 | 51, 52, 55, 57 | rdgisucinc 6362 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦))) |
59 | 58 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦))) |
60 | 38, 50, 59 | 3eqtr4d 2213 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
61 | | peano2 4577 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
62 | | fvres 5518 |
. . . . . . . . 9
⊢ (suc
𝑦 ∈ ω →
((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
63 | 61, 62 | syl 14 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
64 | 63 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦)) |
65 | 60, 64 | eqtr4d 2206 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)) |
66 | 65 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))) |
67 | 66 | expcom 115 |
. . . 4
⊢ (𝑦 ∈ ω → (𝜑 → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)))) |
68 | 18, 21, 24, 33, 67 | finds2 4583 |
. . 3
⊢ (𝑥 ∈ ω → (𝜑 → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥))) |
69 | 68 | impcom 124 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥)) |
70 | 10, 15, 69 | eqfnfvd 5594 |
1
⊢ (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω)) |