Step | Hyp | Ref
| Expression |
1 | | frecfcllem.g |
. . . . . 6
⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) |
2 | | funmpt 5067 |
. . . . . . 7
⊢ Fun
(𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
3 | 2 | a1i 9 |
. . . . . 6
⊢
(((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) → Fun (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) |
4 | | ordom 4436 |
. . . . . . 7
⊢ Ord
ω |
5 | 4 | a1i 9 |
. . . . . 6
⊢
(((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) → Ord
ω) |
6 | | vex 2625 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
7 | | simp2 945 |
. . . . . . . . 9
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑦 ∈ ω) |
8 | | simp3 946 |
. . . . . . . . 9
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓:𝑦⟶𝑆) |
9 | | simp1ll 1007 |
. . . . . . . . . 10
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆) |
10 | | fveq2 5320 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤)) |
11 | 10 | eleq1d 2157 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) ∈ 𝑆 ↔ (𝐹‘𝑤) ∈ 𝑆)) |
12 | 11 | cbvralv 2593 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆) |
13 | 9, 12 | sylib 121 |
. . . . . . . . 9
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆) |
14 | | simp1lr 1008 |
. . . . . . . . 9
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝐴 ∈ 𝑆) |
15 | 7, 8, 13, 14 | frecabcl 6180 |
. . . . . . . 8
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) |
16 | | dmeq 4651 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓) |
17 | 16 | eqeq1d 2097 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚)) |
18 | | fveq1 5319 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → (𝑔‘𝑚) = (𝑓‘𝑚)) |
19 | 18 | fveq2d 5324 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → (𝐹‘(𝑔‘𝑚)) = (𝐹‘(𝑓‘𝑚))) |
20 | 19 | eleq2d 2158 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))) |
21 | 17, 20 | anbi12d 458 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))))) |
22 | 21 | rexbidv 2382 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))))) |
23 | 16 | eqeq1d 2097 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅)) |
24 | 23 | anbi1d 454 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))) |
25 | 22, 24 | orbi12d 743 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴)))) |
26 | 25 | abbidv 2206 |
. . . . . . . . 9
⊢ (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
27 | | eqid 2089 |
. . . . . . . . 9
⊢ (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
28 | 26, 27 | fvmptg 5395 |
. . . . . . . 8
⊢ ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
29 | 6, 15, 28 | sylancr 406 |
. . . . . . 7
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))}) |
30 | 29, 15 | eqeltrd 2165 |
. . . . . 6
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})‘𝑓) ∈ 𝑆) |
31 | | limom 4443 |
. . . . . . . . . 10
⊢ Lim
ω |
32 | | limuni 4234 |
. . . . . . . . . 10
⊢ (Lim
ω → ω = ∪ ω) |
33 | 31, 32 | ax-mp 7 |
. . . . . . . . 9
⊢ ω =
∪ ω |
34 | 33 | eleq2i 2155 |
. . . . . . . 8
⊢ (𝑦 ∈ ω ↔ 𝑦 ∈ ∪ ω) |
35 | | peano2 4425 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
36 | 34, 35 | sylbir 134 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ ω → suc 𝑦 ∈ ω) |
37 | 36 | adantl 272 |
. . . . . 6
⊢
((((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ∪ ω)
→ suc 𝑦 ∈
ω) |
38 | 33 | eleq2i 2155 |
. . . . . . . 8
⊢ (𝑘 ∈ ω ↔ 𝑘 ∈ ∪ ω) |
39 | 38 | biimpi 119 |
. . . . . . 7
⊢ (𝑘 ∈ ω → 𝑘 ∈ ∪ ω) |
40 | 39 | adantl 272 |
. . . . . 6
⊢
(((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ∪
ω) |
41 | 1, 3, 5, 30, 37, 40 | tfrcldm 6144 |
. . . . 5
⊢
(((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom 𝐺) |
42 | 1, 3, 5, 30, 37, 40 | tfrcl 6145 |
. . . . 5
⊢
(((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ∈ 𝑆) |
43 | 41, 42 | jca 301 |
. . . 4
⊢
(((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) ∧ 𝑘 ∈ ω) → (𝑘 ∈ dom 𝐺 ∧ (𝐺‘𝑘) ∈ 𝑆)) |
44 | 43 | ralrimiva 2447 |
. . 3
⊢
((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → ∀𝑘 ∈ ω (𝑘 ∈ dom 𝐺 ∧ (𝐺‘𝑘) ∈ 𝑆)) |
45 | | tfrfun 6101 |
. . . . 5
⊢ Fun
recs((𝑔 ∈ V ↦
{𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) |
46 | 1 | funeqi 5051 |
. . . . 5
⊢ (Fun
𝐺 ↔ Fun recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}))) |
47 | 45, 46 | mpbir 145 |
. . . 4
⊢ Fun 𝐺 |
48 | | ffvresb 5477 |
. . . 4
⊢ (Fun
𝐺 → ((𝐺 ↾
ω):ω⟶𝑆
↔ ∀𝑘 ∈
ω (𝑘 ∈ dom 𝐺 ∧ (𝐺‘𝑘) ∈ 𝑆))) |
49 | 47, 48 | ax-mp 7 |
. . 3
⊢ ((𝐺 ↾
ω):ω⟶𝑆
↔ ∀𝑘 ∈
ω (𝑘 ∈ dom 𝐺 ∧ (𝐺‘𝑘) ∈ 𝑆)) |
50 | 44, 49 | sylibr 133 |
. 2
⊢
((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝐺 ↾ ω):ω⟶𝑆) |
51 | | df-frec 6172 |
. . . 4
⊢
frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω) |
52 | 1 | reseq1i 4724 |
. . . 4
⊢ (𝐺 ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω) |
53 | 51, 52 | eqtr4i 2112 |
. . 3
⊢
frec(𝐹, 𝐴) = (𝐺 ↾ ω) |
54 | 53 | feq1i 5169 |
. 2
⊢
(frec(𝐹, 𝐴):ω⟶𝑆 ↔ (𝐺 ↾ ω):ω⟶𝑆) |
55 | 50, 54 | sylibr 133 |
1
⊢
((∀𝑧 ∈
𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) |