Step | Hyp | Ref
| Expression |
1 | | frfnom 7530 |
. . . . . . . 8
⊢
(rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω |
2 | | axdclem2.1 |
. . . . . . . . 9
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
3 | 2 | fneq1i 5985 |
. . . . . . . 8
⊢ (𝐹 Fn ω ↔ (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω) |
4 | 1, 3 | mpbir 221 |
. . . . . . 7
⊢ 𝐹 Fn ω |
5 | 4 | a1i 11 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 Fn ω) |
6 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘𝑛) = (𝐹‘∅)) |
7 | | suceq 5790 |
. . . . . . . . . . . 12
⊢ (𝑛 = ∅ → suc 𝑛 = suc ∅) |
8 | 7 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘suc 𝑛) = (𝐹‘suc ∅)) |
9 | 6, 8 | breq12d 4666 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘∅)𝑥(𝐹‘suc ∅))) |
10 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
11 | | suceq 5790 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘) |
12 | 11 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc 𝑘)) |
13 | 10, 12 | breq12d 4666 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘𝑘)𝑥(𝐹‘suc 𝑘))) |
14 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘𝑛) = (𝐹‘suc 𝑘)) |
15 | | suceq 5790 |
. . . . . . . . . . . 12
⊢ (𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘) |
16 | 15 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc suc 𝑘)) |
17 | 14, 16 | breq12d 4666 |
. . . . . . . . . 10
⊢ (𝑛 = suc 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
18 | 2 | fveq1i 6192 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘∅) = ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾
ω)‘∅) |
19 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑠 ∈ V |
20 | | fr0g 7531 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ V → ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠 |
22 | 18, 21 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘∅) = 𝑠 |
23 | 22 | breq1i 4660 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘∅)𝑥𝑧 ↔ 𝑠𝑥𝑧) |
24 | 23 | biimpri 218 |
. . . . . . . . . . . . 13
⊢ (𝑠𝑥𝑧 → (𝐹‘∅)𝑥𝑧) |
25 | 24 | eximi 1762 |
. . . . . . . . . . . 12
⊢
(∃𝑧 𝑠𝑥𝑧 → ∃𝑧(𝐹‘∅)𝑥𝑧) |
26 | | peano1 7085 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
27 | 2 | axdclem 9341 |
. . . . . . . . . . . . 13
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (∅ ∈ ω →
(𝐹‘∅)𝑥(𝐹‘suc ∅))) |
28 | 26, 27 | mpi 20 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
29 | 25, 28 | syl3an3 1361 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧 𝑠𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
30 | 29 | 3com23 1271 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
31 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑘) ∈ V |
32 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘suc 𝑘) ∈ V |
33 | 31, 32 | brelrn 5356 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ ran 𝑥) |
34 | | ssel 3597 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘suc 𝑘) ∈ ran 𝑥 → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
35 | 33, 34 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
36 | 32 | eldm 5321 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘suc 𝑘) ∈ dom 𝑥 ↔ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) |
37 | 35, 36 | syl6ib 241 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
38 | 37 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
39 | | peano2 7086 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
40 | 2 | axdclem 9341 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (suc 𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
41 | 39, 40 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
42 | 41 | 3expia 1267 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
43 | 42 | com3r 87 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
44 | 43 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
45 | 38, 44 | syld 47 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
46 | 45 | 3adantr2 1221 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
47 | 46 | ex 450 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
48 | 9, 13, 17, 30, 47 | finds2 7094 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
49 | 48 | com12 32 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
50 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐹‘𝑛) ∈ V |
51 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐹‘suc 𝑛) ∈ V |
52 | 50, 51 | breldm 5329 |
. . . . . . . 8
⊢ ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) → (𝐹‘𝑛) ∈ dom 𝑥) |
53 | 49, 52 | syl6 35 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛) ∈ dom 𝑥)) |
54 | 53 | ralrimiv 2965 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥) |
55 | | ffnfv 6388 |
. . . . . 6
⊢ (𝐹:ω⟶dom 𝑥 ↔ (𝐹 Fn ω ∧ ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥)) |
56 | 5, 54, 55 | sylanbrc 698 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹:ω⟶dom 𝑥) |
57 | | omex 8540 |
. . . . . 6
⊢ ω
∈ V |
58 | 57 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ω ∈ V) |
59 | | vex 3203 |
. . . . . . 7
⊢ 𝑥 ∈ V |
60 | 59 | dmex 7099 |
. . . . . 6
⊢ dom 𝑥 ∈ V |
61 | 60 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → dom 𝑥 ∈ V) |
62 | | fex2 7121 |
. . . . 5
⊢ ((𝐹:ω⟶dom 𝑥 ∧ ω ∈ V ∧
dom 𝑥 ∈ V) →
𝐹 ∈
V) |
63 | 56, 58, 61, 62 | syl3anc 1326 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 ∈ V) |
64 | 49 | ralrimiv 2965 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛)) |
65 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛)) |
66 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘suc 𝑛) = (𝐹‘suc 𝑛)) |
67 | 65, 66 | breq12d 4666 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
68 | 67 | ralbidv 2986 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
69 | 68 | spcegv 3294 |
. . . 4
⊢ (𝐹 ∈ V → (∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
70 | 63, 64, 69 | sylc 65 |
. . 3
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
71 | 70 | 3exp 1264 |
. 2
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)))) |
72 | 60 | pwex 4848 |
. . 3
⊢ 𝒫
dom 𝑥 ∈
V |
73 | 72 | ac4c 9298 |
. 2
⊢
∃𝑔∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) |
74 | 71, 73 | exlimiiv 1859 |
1
⊢
(∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |