Step | Hyp | Ref
| Expression |
1 | | freccl.b |
. 2
⊢ (𝜑 → 𝐵 ∈ ω) |
2 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = 𝐵 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘𝐵)) |
3 | 2 | eleq1d 2106 |
. . . 4
⊢ (𝑥 = 𝐵 → ((frec(𝐹, 𝐴)‘𝑥) ∈ 𝑆 ↔ (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆)) |
4 | 3 | imbi2d 219 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝜑 → (frec(𝐹, 𝐴)‘𝑥) ∈ 𝑆) ↔ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆))) |
5 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = ∅ → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘∅)) |
6 | 5 | eleq1d 2106 |
. . . 4
⊢ (𝑥 = ∅ → ((frec(𝐹, 𝐴)‘𝑥) ∈ 𝑆 ↔ (frec(𝐹, 𝐴)‘∅) ∈ 𝑆)) |
7 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘𝑦)) |
8 | 7 | eleq1d 2106 |
. . . 4
⊢ (𝑥 = 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) ∈ 𝑆 ↔ (frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆)) |
9 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘suc 𝑦)) |
10 | 9 | eleq1d 2106 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) ∈ 𝑆 ↔ (frec(𝐹, 𝐴)‘suc 𝑦) ∈ 𝑆)) |
11 | | freccl.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
12 | | frec0g 5983 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → (frec(𝐹, 𝐴)‘∅) = 𝐴) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = 𝐴) |
14 | 13, 11 | eqeltrd 2114 |
. . . 4
⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) ∈ 𝑆) |
15 | | freccl.ex |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑧(𝐹‘𝑧) ∈ V) |
16 | | frecfnom 5986 |
. . . . . . . . . 10
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴) Fn ω) |
17 | 15, 11, 16 | syl2anc 391 |
. . . . . . . . 9
⊢ (𝜑 → frec(𝐹, 𝐴) Fn ω) |
18 | | funfvex 5192 |
. . . . . . . . . 10
⊢ ((Fun
frec(𝐹, 𝐴) ∧ 𝑦 ∈ dom frec(𝐹, 𝐴)) → (frec(𝐹, 𝐴)‘𝑦) ∈ V) |
19 | 18 | funfni 4999 |
. . . . . . . . 9
⊢
((frec(𝐹, 𝐴) Fn ω ∧ 𝑦 ∈ ω) →
(frec(𝐹, 𝐴)‘𝑦) ∈ V) |
20 | 17, 19 | sylan 267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘𝑦) ∈ V) |
21 | | isset 2561 |
. . . . . . . 8
⊢
((frec(𝐹, 𝐴)‘𝑦) ∈ V ↔ ∃𝑧 𝑧 = (frec(𝐹, 𝐴)‘𝑦)) |
22 | 20, 21 | sylib 127 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ∃𝑧 𝑧 = (frec(𝐹, 𝐴)‘𝑦)) |
23 | | freccl.cl |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) |
24 | 23 | ex 108 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑆 → (𝐹‘𝑧) ∈ 𝑆)) |
25 | 24 | adantr 261 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 = (frec(𝐹, 𝐴)‘𝑦)) → (𝑧 ∈ 𝑆 → (𝐹‘𝑧) ∈ 𝑆)) |
26 | | eleq1 2100 |
. . . . . . . . . . . 12
⊢ (𝑧 = (frec(𝐹, 𝐴)‘𝑦) → (𝑧 ∈ 𝑆 ↔ (frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆)) |
27 | 26 | adantl 262 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 = (frec(𝐹, 𝐴)‘𝑦)) → (𝑧 ∈ 𝑆 ↔ (frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆)) |
28 | | fveq2 5178 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (frec(𝐹, 𝐴)‘𝑦) → (𝐹‘𝑧) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
29 | 28 | eleq1d 2106 |
. . . . . . . . . . . 12
⊢ (𝑧 = (frec(𝐹, 𝐴)‘𝑦) → ((𝐹‘𝑧) ∈ 𝑆 ↔ (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆)) |
30 | 29 | adantl 262 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 = (frec(𝐹, 𝐴)‘𝑦)) → ((𝐹‘𝑧) ∈ 𝑆 ↔ (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆)) |
31 | 25, 27, 30 | 3imtr3d 191 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 = (frec(𝐹, 𝐴)‘𝑦)) → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆)) |
32 | 31 | ex 108 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 = (frec(𝐹, 𝐴)‘𝑦) → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆))) |
33 | 32 | exlimdv 1700 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑧 𝑧 = (frec(𝐹, 𝐴)‘𝑦) → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆))) |
34 | 33 | adantr 261 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (∃𝑧 𝑧 = (frec(𝐹, 𝐴)‘𝑦) → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆))) |
35 | 22, 34 | mpd 13 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆)) |
36 | 15 | adantr 261 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ∀𝑧(𝐹‘𝑧) ∈ V) |
37 | 11 | adantr 261 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝑆) |
38 | | simpr 103 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ ω) |
39 | | frecsuc 5991 |
. . . . . . . 8
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑆 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
40 | 36, 37, 38, 39 | syl3anc 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦))) |
41 | 40 | eleq1d 2106 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘suc 𝑦) ∈ 𝑆 ↔ (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) ∈ 𝑆)) |
42 | 35, 41 | sylibrd 158 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (frec(𝐹, 𝐴)‘suc 𝑦) ∈ 𝑆)) |
43 | 42 | expcom 109 |
. . . 4
⊢ (𝑦 ∈ ω → (𝜑 → ((frec(𝐹, 𝐴)‘𝑦) ∈ 𝑆 → (frec(𝐹, 𝐴)‘suc 𝑦) ∈ 𝑆))) |
44 | 6, 8, 10, 14, 43 | finds2 4324 |
. . 3
⊢ (𝑥 ∈ ω → (𝜑 → (frec(𝐹, 𝐴)‘𝑥) ∈ 𝑆)) |
45 | 4, 44 | vtoclga 2619 |
. 2
⊢ (𝐵 ∈ ω → (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆)) |
46 | 1, 45 | mpcom 32 |
1
⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) |