Step | Hyp | Ref
| Expression |
1 | | frecsuc.1 |
. . . . . . . 8
⊢ F = FRec (G, I) |
2 | | frecsuc.2 |
. . . . . . . 8
⊢ (φ → G ∈ Funs ) |
3 | | frecsuc.3 |
. . . . . . . 8
⊢ (φ → I ∈ dom G) |
4 | | frecsuc.4 |
. . . . . . . 8
⊢ (φ → ran G ⊆ dom G) |
5 | 1, 2, 3, 4 | fnfrec 6320 |
. . . . . . 7
⊢ (φ → F Fn Nn
) |
6 | | fnfun 5181 |
. . . . . . 7
⊢ (F Fn Nn → Fun
F) |
7 | 5, 6 | syl 15 |
. . . . . 6
⊢ (φ → Fun F) |
8 | | frecsuc.5 |
. . . . . . 7
⊢ (φ → X ∈ Nn ) |
9 | 1, 2, 3, 4 | dmfrec 6316 |
. . . . . . 7
⊢ (φ → dom F = Nn
) |
10 | 8, 9 | eleqtrrd 2430 |
. . . . . 6
⊢ (φ → X ∈ dom F) |
11 | | funfvop 5400 |
. . . . . 6
⊢ ((Fun F ∧ X ∈ dom F) → 〈X, (F ‘X)〉 ∈ F) |
12 | 7, 10, 11 | syl2anc 642 |
. . . . 5
⊢ (φ → 〈X, (F ‘X)〉 ∈ F) |
13 | | eqid 2353 |
. . . . . 6
⊢ (X +c 1c) =
(X +c
1c) |
14 | | peano2 4403 |
. . . . . . . 8
⊢ (X ∈ Nn → (X
+c 1c) ∈
Nn ) |
15 | 8, 14 | syl 15 |
. . . . . . 7
⊢ (φ → (X +c 1c) ∈ Nn
) |
16 | | addceq1 4383 |
. . . . . . . . 9
⊢ (w = X →
(w +c
1c) = (X
+c 1c)) |
17 | 16 | eqeq2d 2364 |
. . . . . . . 8
⊢ (w = X →
(y = (w
+c 1c) ↔ y = (X
+c 1c))) |
18 | | eqeq1 2359 |
. . . . . . . 8
⊢ (y = (X
+c 1c) → (y = (X
+c 1c) ↔ (X +c 1c) =
(X +c
1c))) |
19 | | mptv 5718 |
. . . . . . . 8
⊢ (w ∈ V ↦ (w
+c 1c)) = {〈w, y〉 ∣ y =
(w +c
1c)} |
20 | 17, 18, 19 | brabg 4706 |
. . . . . . 7
⊢ ((X ∈ Nn ∧ (X +c 1c) ∈ Nn ) →
(X(w
∈ V ↦
(w +c
1c))(X
+c 1c) ↔ (X +c 1c) =
(X +c
1c))) |
21 | 8, 15, 20 | syl2anc 642 |
. . . . . 6
⊢ (φ → (X(w ∈ V ↦ (w +c
1c))(X
+c 1c) ↔ (X +c 1c) =
(X +c
1c))) |
22 | 13, 21 | mpbiri 224 |
. . . . 5
⊢ (φ → X(w ∈ V ↦ (w +c
1c))(X
+c 1c)) |
23 | | elfunsi 5831 |
. . . . . . . 8
⊢ (G ∈ Funs → Fun G) |
24 | 2, 23 | syl 15 |
. . . . . . 7
⊢ (φ → Fun G) |
25 | 3 | snssd 3853 |
. . . . . . . . 9
⊢ (φ → {I} ⊆ dom G) |
26 | 4, 25 | unssd 3439 |
. . . . . . . 8
⊢ (φ → (ran G ∪ {I})
⊆ dom G) |
27 | 1 | frecxpg 6315 |
. . . . . . . . . . . 12
⊢ (G ∈ Funs → F ⊆ ( Nn × (ran
G ∪ {I}))) |
28 | 2, 27 | syl 15 |
. . . . . . . . . . 11
⊢ (φ → F ⊆ ( Nn × (ran G
∪ {I}))) |
29 | | rnss 4959 |
. . . . . . . . . . 11
⊢ (F ⊆ ( Nn × (ran G
∪ {I})) → ran F ⊆ ran ( Nn × (ran G
∪ {I}))) |
30 | 28, 29 | syl 15 |
. . . . . . . . . 10
⊢ (φ → ran F ⊆ ran ( Nn × (ran G
∪ {I}))) |
31 | | rnxpss 5053 |
. . . . . . . . . 10
⊢ ran ( Nn × (ran G
∪ {I})) ⊆ (ran G ∪
{I}) |
32 | 30, 31 | syl6ss 3284 |
. . . . . . . . 9
⊢ (φ → ran F ⊆ (ran G ∪ {I})) |
33 | | fvelrn 5413 |
. . . . . . . . . 10
⊢ ((Fun F ∧ X ∈ dom F) → (F
‘X) ∈ ran F) |
34 | 7, 10, 33 | syl2anc 642 |
. . . . . . . . 9
⊢ (φ → (F ‘X)
∈ ran F) |
35 | 32, 34 | sseldd 3274 |
. . . . . . . 8
⊢ (φ → (F ‘X)
∈ (ran G
∪ {I})) |
36 | 26, 35 | sseldd 3274 |
. . . . . . 7
⊢ (φ → (F ‘X)
∈ dom G) |
37 | | funfvop 5400 |
. . . . . . 7
⊢ ((Fun G ∧ (F ‘X)
∈ dom G)
→ 〈(F ‘X),
(G ‘(F ‘X))〉 ∈ G) |
38 | 24, 36, 37 | syl2anc 642 |
. . . . . 6
⊢ (φ → 〈(F
‘X), (G ‘(F
‘X))〉 ∈ G) |
39 | | df-br 4640 |
. . . . . 6
⊢ ((F ‘X)G(G ‘(F
‘X)) ↔ 〈(F
‘X), (G ‘(F
‘X))〉 ∈ G) |
40 | 38, 39 | sylibr 203 |
. . . . 5
⊢ (φ → (F ‘X)G(G ‘(F
‘X))) |
41 | | breq1 4642 |
. . . . . . 7
⊢ (y = 〈X, (F
‘X)〉 → (y
PProd ((w
∈ V ↦
(w +c
1c)), G)〈(X
+c 1c), (G ‘(F
‘X))〉 ↔ 〈X, (F ‘X)〉 PProd ((w ∈ V ↦ (w
+c 1c)), G)〈(X +c 1c),
(G ‘(F ‘X))〉)) |
42 | | qrpprod 5836 |
. . . . . . 7
⊢ (〈X, (F ‘X)〉 PProd ((w ∈ V ↦ (w
+c 1c)), G)〈(X +c 1c),
(G ‘(F ‘X))〉 ↔
(X(w
∈ V ↦
(w +c
1c))(X
+c 1c) ∧
(F ‘X)G(G ‘(F
‘X)))) |
43 | 41, 42 | syl6bb 252 |
. . . . . 6
⊢ (y = 〈X, (F
‘X)〉 → (y
PProd ((w
∈ V ↦
(w +c
1c)), G)〈(X
+c 1c), (G ‘(F
‘X))〉 ↔ (X(w ∈ V ↦ (w +c
1c))(X
+c 1c) ∧
(F ‘X)G(G ‘(F
‘X))))) |
44 | 43 | rspcev 2955 |
. . . . 5
⊢ ((〈X, (F ‘X)〉 ∈ F ∧ (X(w ∈ V ↦ (w +c
1c))(X
+c 1c) ∧
(F ‘X)G(G ‘(F
‘X)))) → ∃y ∈ F y PProd ((w ∈ V ↦ (w
+c 1c)), G)〈(X +c 1c),
(G ‘(F ‘X))〉) |
45 | 12, 22, 40, 44 | syl12anc 1180 |
. . . 4
⊢ (φ → ∃y ∈ F y PProd ((w ∈ V ↦ (w
+c 1c)), G)〈(X +c 1c),
(G ‘(F ‘X))〉) |
46 | 45 | olcd 382 |
. . 3
⊢ (φ → (〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ {〈0c, I〉} ∨ ∃y ∈ F y PProd ((w ∈ V ↦ (w +c 1c)),
G)〈(X
+c 1c), (G ‘(F
‘X))〉)) |
47 | | snex 4111 |
. . . 4
⊢ {〈0c, I〉} ∈ V |
48 | | csucex 6259 |
. . . . 5
⊢ (w ∈ V ↦ (w
+c 1c)) ∈
V |
49 | | pprodexg 5837 |
. . . . 5
⊢ (((w ∈ V ↦ (w
+c 1c)) ∈
V ∧ G
∈ Funs ) →
PProd ((w
∈ V ↦
(w +c
1c)), G) ∈ V) |
50 | 48, 2, 49 | sylancr 644 |
. . . 4
⊢ (φ → PProd
((w ∈ V
↦ (w
+c 1c)), G) ∈
V) |
51 | | df-frec 6310 |
. . . . . 6
⊢ FRec (G, I) = Clos1 ({〈0c, I〉}, PProd ((w ∈ V ↦ (w +c 1c)),
G)) |
52 | 1, 51 | eqtri 2373 |
. . . . 5
⊢ F = Clos1 ({〈0c, I〉}, PProd ((w ∈ V ↦ (w +c 1c)),
G)) |
53 | 52 | clos1basesucg 5884 |
. . . 4
⊢ (({〈0c, I〉} ∈ V ∧ PProd ((w ∈ V ↦ (w +c 1c)),
G) ∈ V)
→ (〈(X +c 1c),
(G ‘(F ‘X))〉 ∈ F ↔
(〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ {〈0c, I〉} ∨ ∃y ∈ F y PProd ((w ∈ V ↦ (w +c 1c)),
G)〈(X
+c 1c), (G ‘(F
‘X))〉))) |
54 | 47, 50, 53 | sylancr 644 |
. . 3
⊢ (φ → (〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ F ↔ (〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ {〈0c, I〉} ∨ ∃y ∈ F y PProd ((w ∈ V ↦ (w +c 1c)),
G)〈(X
+c 1c), (G ‘(F
‘X))〉))) |
55 | 46, 54 | mpbird 223 |
. 2
⊢ (φ → 〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ F) |
56 | | fnopfvb 5359 |
. . 3
⊢ ((F Fn Nn ∧ (X
+c 1c) ∈
Nn ) → ((F ‘(X
+c 1c)) = (G ‘(F
‘X)) ↔ 〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ F)) |
57 | 5, 15, 56 | syl2anc 642 |
. 2
⊢ (φ → ((F ‘(X
+c 1c)) = (G ‘(F
‘X)) ↔ 〈(X
+c 1c), (G ‘(F
‘X))〉 ∈ F)) |
58 | 55, 57 | mpbird 223 |
1
⊢ (φ → (F ‘(X
+c 1c)) = (G ‘(F
‘X))) |