Step | Hyp | Ref
| Expression |
1 | | frfnom 7925 |
. . . . . . . 8
⊢
(rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω |
2 | | axdclem2.1 |
. . . . . . . . 9
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
3 | 2 | fneq1i 6323 |
. . . . . . . 8
⊢ (𝐹 Fn ω ↔ (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω) |
4 | 1, 3 | mpbir 232 |
. . . . . . 7
⊢ 𝐹 Fn ω |
5 | 4 | a1i 11 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 Fn ω) |
6 | | fveq2 6541 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘𝑛) = (𝐹‘∅)) |
7 | | suceq 6134 |
. . . . . . . . . . . 12
⊢ (𝑛 = ∅ → suc 𝑛 = suc ∅) |
8 | 7 | fveq2d 6545 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘suc 𝑛) = (𝐹‘suc ∅)) |
9 | 6, 8 | breq12d 4977 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘∅)𝑥(𝐹‘suc ∅))) |
10 | | fveq2 6541 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
11 | | suceq 6134 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘) |
12 | 11 | fveq2d 6545 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc 𝑘)) |
13 | 10, 12 | breq12d 4977 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘𝑘)𝑥(𝐹‘suc 𝑘))) |
14 | | fveq2 6541 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘𝑛) = (𝐹‘suc 𝑘)) |
15 | | suceq 6134 |
. . . . . . . . . . . 12
⊢ (𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘) |
16 | 15 | fveq2d 6545 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc suc 𝑘)) |
17 | 14, 16 | breq12d 4977 |
. . . . . . . . . 10
⊢ (𝑛 = suc 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
18 | 2 | fveq1i 6542 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘∅) = ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾
ω)‘∅) |
19 | | fr0g 7926 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ V → ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠) |
20 | 19 | elv 3441 |
. . . . . . . . . . . . . . . 16
⊢
((rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠 |
21 | 18, 20 | eqtri 2818 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘∅) = 𝑠 |
22 | 21 | breq1i 4971 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘∅)𝑥𝑧 ↔ 𝑠𝑥𝑧) |
23 | 22 | biimpri 229 |
. . . . . . . . . . . . 13
⊢ (𝑠𝑥𝑧 → (𝐹‘∅)𝑥𝑧) |
24 | 23 | eximi 1817 |
. . . . . . . . . . . 12
⊢
(∃𝑧 𝑠𝑥𝑧 → ∃𝑧(𝐹‘∅)𝑥𝑧) |
25 | | peano1 7460 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
26 | 2 | axdclem 9790 |
. . . . . . . . . . . . 13
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (∅ ∈ ω →
(𝐹‘∅)𝑥(𝐹‘suc ∅))) |
27 | 25, 26 | mpi 20 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
28 | 24, 27 | syl3an3 1158 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧 𝑠𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
29 | 28 | 3com23 1119 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
30 | | fvex 6554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑘) ∈ V |
31 | | fvex 6554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘suc 𝑘) ∈ V |
32 | 30, 31 | brelrn 5697 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ ran 𝑥) |
33 | | ssel 3885 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘suc 𝑘) ∈ ran 𝑥 → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
34 | 32, 33 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
35 | 31 | eldm 5658 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘suc 𝑘) ∈ dom 𝑥 ↔ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) |
36 | 34, 35 | syl6ib 252 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
37 | 36 | ad2antll 725 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
38 | | peano2 7461 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
39 | 2 | axdclem 9790 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (suc 𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
40 | 38, 39 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
41 | 40 | 3expia 1114 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
42 | 41 | com3r 87 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
43 | 42 | imp 407 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
44 | 37, 43 | syld 47 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
45 | 44 | 3adantr2 1163 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
46 | 45 | ex 413 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
47 | 9, 13, 17, 29, 46 | finds2 7469 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
48 | 47 | com12 32 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
49 | | fvex 6554 |
. . . . . . . . 9
⊢ (𝐹‘𝑛) ∈ V |
50 | | fvex 6554 |
. . . . . . . . 9
⊢ (𝐹‘suc 𝑛) ∈ V |
51 | 49, 50 | breldm 5666 |
. . . . . . . 8
⊢ ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) → (𝐹‘𝑛) ∈ dom 𝑥) |
52 | 48, 51 | syl6 35 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛) ∈ dom 𝑥)) |
53 | 52 | ralrimiv 3147 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥) |
54 | | ffnfv 6748 |
. . . . . 6
⊢ (𝐹:ω⟶dom 𝑥 ↔ (𝐹 Fn ω ∧ ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥)) |
55 | 5, 53, 54 | sylanbrc 583 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹:ω⟶dom 𝑥) |
56 | | omex 8955 |
. . . . . 6
⊢ ω
∈ V |
57 | 56 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ω ∈ V) |
58 | | vex 3439 |
. . . . . . 7
⊢ 𝑥 ∈ V |
59 | 58 | dmex 7475 |
. . . . . 6
⊢ dom 𝑥 ∈ V |
60 | 59 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → dom 𝑥 ∈ V) |
61 | | fex2 7497 |
. . . . 5
⊢ ((𝐹:ω⟶dom 𝑥 ∧ ω ∈ V ∧
dom 𝑥 ∈ V) →
𝐹 ∈
V) |
62 | 55, 57, 60, 61 | syl3anc 1364 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 ∈ V) |
63 | 48 | ralrimiv 3147 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛)) |
64 | | fveq1 6540 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛)) |
65 | | fveq1 6540 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘suc 𝑛) = (𝐹‘suc 𝑛)) |
66 | 64, 65 | breq12d 4977 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
67 | 66 | ralbidv 3163 |
. . . 4
⊢ (𝑓 = 𝐹 → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
68 | 62, 63, 67 | elabd 3605 |
. . 3
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
69 | 68 | 3exp 1112 |
. 2
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)))) |
70 | 59 | pwex 5175 |
. . 3
⊢ 𝒫
dom 𝑥 ∈
V |
71 | 70 | ac4c 9747 |
. 2
⊢
∃𝑔∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) |
72 | 69, 71 | exlimiiv 1910 |
1
⊢
(∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |