Step | Hyp | Ref
| Expression |
1 | | frfnom 7417 |
. . . . . . . 8
⊢
(rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω |
2 | | axdclem2.1 |
. . . . . . . . 9
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
3 | 2 | fneq1i 5899 |
. . . . . . . 8
⊢ (𝐹 Fn ω ↔ (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω) |
4 | 1, 3 | mpbir 220 |
. . . . . . 7
⊢ 𝐹 Fn ω |
5 | 4 | a1i 11 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 Fn ω) |
6 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘𝑛) = (𝐹‘∅)) |
7 | | suceq 5707 |
. . . . . . . . . . . 12
⊢ (𝑛 = ∅ → suc 𝑛 = suc ∅) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘suc 𝑛) = (𝐹‘suc ∅)) |
9 | 6, 8 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘∅)𝑥(𝐹‘suc ∅))) |
10 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
11 | | suceq 5707 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc 𝑘)) |
13 | 10, 12 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘𝑘)𝑥(𝐹‘suc 𝑘))) |
14 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘𝑛) = (𝐹‘suc 𝑘)) |
15 | | suceq 5707 |
. . . . . . . . . . . 12
⊢ (𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc suc 𝑘)) |
17 | 14, 16 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑛 = suc 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
18 | 2 | fveq1i 6104 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘∅) = ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾
ω)‘∅) |
19 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑠 ∈ V |
20 | | fr0g 7418 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ V → ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠 |
22 | 18, 21 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘∅) = 𝑠 |
23 | 22 | breq1i 4590 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘∅)𝑥𝑧 ↔ 𝑠𝑥𝑧) |
24 | 23 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ (𝑠𝑥𝑧 → (𝐹‘∅)𝑥𝑧) |
25 | 24 | eximi 1752 |
. . . . . . . . . . . 12
⊢
(∃𝑧 𝑠𝑥𝑧 → ∃𝑧(𝐹‘∅)𝑥𝑧) |
26 | | peano1 6977 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
27 | 2 | axdclem 9224 |
. . . . . . . . . . . . 13
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (∅ ∈ ω →
(𝐹‘∅)𝑥(𝐹‘suc ∅))) |
28 | 26, 27 | mpi 20 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
29 | 25, 28 | syl3an3 1353 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧 𝑠𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
30 | 29 | 3com23 1263 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
31 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑘) ∈ V |
32 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘suc 𝑘) ∈ V |
33 | 31, 32 | brelrn 5277 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ ran 𝑥) |
34 | | ssel 3562 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘suc 𝑘) ∈ ran 𝑥 → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
35 | 33, 34 | syl5 33 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
36 | 32 | eldm 5243 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘suc 𝑘) ∈ dom 𝑥 ↔ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) |
37 | 35, 36 | syl6ib 240 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
38 | 37 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
39 | | peano2 6978 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
40 | 2 | axdclem 9224 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (suc 𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
41 | 39, 40 | syl5 33 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
42 | 41 | 3expia 1259 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
43 | 42 | com3r 85 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
44 | 43 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
45 | 38, 44 | syld 46 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
46 | 45 | 3adantr2 1214 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
47 | 46 | ex 449 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
48 | 9, 13, 17, 30, 47 | finds2 6986 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
49 | 48 | com12 32 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
50 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐹‘𝑛) ∈ V |
51 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐹‘suc 𝑛) ∈ V |
52 | 50, 51 | breldm 5251 |
. . . . . . . 8
⊢ ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) → (𝐹‘𝑛) ∈ dom 𝑥) |
53 | 49, 52 | syl6 34 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛) ∈ dom 𝑥)) |
54 | 53 | ralrimiv 2948 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥) |
55 | | ffnfv 6295 |
. . . . . 6
⊢ (𝐹:ω⟶dom 𝑥 ↔ (𝐹 Fn ω ∧ ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥)) |
56 | 5, 54, 55 | sylanbrc 695 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹:ω⟶dom 𝑥) |
57 | | omex 8423 |
. . . . . 6
⊢ ω
∈ V |
58 | 57 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ω ∈ V) |
59 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
60 | 59 | dmex 6991 |
. . . . . 6
⊢ dom 𝑥 ∈ V |
61 | 60 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → dom 𝑥 ∈ V) |
62 | | fex2 7014 |
. . . . 5
⊢ ((𝐹:ω⟶dom 𝑥 ∧ ω ∈ V ∧
dom 𝑥 ∈ V) →
𝐹 ∈
V) |
63 | 56, 58, 61, 62 | syl3anc 1318 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 ∈ V) |
64 | 49 | ralrimiv 2948 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛)) |
65 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛)) |
66 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘suc 𝑛) = (𝐹‘suc 𝑛)) |
67 | 65, 66 | breq12d 4596 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
68 | 67 | ralbidv 2969 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
69 | 68 | spcegv 3267 |
. . . 4
⊢ (𝐹 ∈ V → (∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
70 | 63, 64, 69 | sylc 63 |
. . 3
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
71 | 70 | 3exp 1256 |
. 2
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)))) |
72 | 60 | pwex 4774 |
. . 3
⊢ 𝒫
dom 𝑥 ∈
V |
73 | 72 | ac4c 9181 |
. 2
⊢
∃𝑔∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) |
74 | 71, 73 | exlimiiv 1846 |
1
⊢
(∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |