Step | Hyp | Ref
| Expression |
1 | | frfnom 8064 |
. . . . . . . 8
⊢
(rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω |
2 | | axdclem2.1 |
. . . . . . . . 9
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
3 | 2 | fneq1i 6445 |
. . . . . . . 8
⊢ (𝐹 Fn ω ↔ (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω) |
4 | 1, 3 | mpbir 233 |
. . . . . . 7
⊢ 𝐹 Fn ω |
5 | 4 | a1i 11 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 Fn ω) |
6 | | fveq2 6665 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘𝑛) = (𝐹‘∅)) |
7 | | suceq 6251 |
. . . . . . . . . . . 12
⊢ (𝑛 = ∅ → suc 𝑛 = suc ∅) |
8 | 7 | fveq2d 6669 |
. . . . . . . . . . 11
⊢ (𝑛 = ∅ → (𝐹‘suc 𝑛) = (𝐹‘suc ∅)) |
9 | 6, 8 | breq12d 5072 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘∅)𝑥(𝐹‘suc ∅))) |
10 | | fveq2 6665 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
11 | | suceq 6251 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘) |
12 | 11 | fveq2d 6669 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc 𝑘)) |
13 | 10, 12 | breq12d 5072 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘𝑘)𝑥(𝐹‘suc 𝑘))) |
14 | | fveq2 6665 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘𝑛) = (𝐹‘suc 𝑘)) |
15 | | suceq 6251 |
. . . . . . . . . . . 12
⊢ (𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘) |
16 | 15 | fveq2d 6669 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc suc 𝑘)) |
17 | 14, 16 | breq12d 5072 |
. . . . . . . . . 10
⊢ (𝑛 = suc 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
18 | 2 | fveq1i 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘∅) = ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾
ω)‘∅) |
19 | | fr0g 8065 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ V → ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠) |
20 | 19 | elv 3500 |
. . . . . . . . . . . . . . . 16
⊢
((rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠 |
21 | 18, 20 | eqtri 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘∅) = 𝑠 |
22 | 21 | breq1i 5066 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘∅)𝑥𝑧 ↔ 𝑠𝑥𝑧) |
23 | 22 | biimpri 230 |
. . . . . . . . . . . . 13
⊢ (𝑠𝑥𝑧 → (𝐹‘∅)𝑥𝑧) |
24 | 23 | eximi 1831 |
. . . . . . . . . . . 12
⊢
(∃𝑧 𝑠𝑥𝑧 → ∃𝑧(𝐹‘∅)𝑥𝑧) |
25 | | peano1 7595 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
26 | 2 | axdclem 9935 |
. . . . . . . . . . . . 13
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (∅ ∈ ω →
(𝐹‘∅)𝑥(𝐹‘suc ∅))) |
27 | 25, 26 | mpi 20 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
28 | 24, 27 | syl3an3 1161 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧 𝑠𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
29 | 28 | 3com23 1122 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) |
30 | | fvex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑘) ∈ V |
31 | | fvex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘suc 𝑘) ∈ V |
32 | 30, 31 | brelrn 5807 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ ran 𝑥) |
33 | | ssel 3961 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘suc 𝑘) ∈ ran 𝑥 → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
34 | 32, 33 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ dom 𝑥)) |
35 | 31 | eldm 5764 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘suc 𝑘) ∈ dom 𝑥 ↔ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) |
36 | 34, 35 | syl6ib 253 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
37 | 36 | ad2antll 727 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) |
38 | | peano2 7596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
39 | 2 | axdclem 9935 |
. . . . . . . . . . . . . . . . 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 1117 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
42 | 41 | com3r 87 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
43 | 42 | imp 409 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
44 | 37, 43 | syld 47 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
45 | 44 | 3adantr2 1166 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) |
46 | 45 | ex 415 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) |
47 | 9, 13, 17, 29, 46 | finds2 7604 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
48 | 47 | com12 32 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
49 | | fvex 6678 |
. . . . . . . . 9
⊢ (𝐹‘𝑛) ∈ V |
50 | | fvex 6678 |
. . . . . . . . 9
⊢ (𝐹‘suc 𝑛) ∈ V |
51 | 49, 50 | breldm 5772 |
. . . . . . . 8
⊢ ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) → (𝐹‘𝑛) ∈ dom 𝑥) |
52 | 48, 51 | syl6 35 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛) ∈ dom 𝑥)) |
53 | 52 | ralrimiv 3181 |
. . . . . 6
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥) |
54 | | ffnfv 6877 |
. . . . . 6
⊢ (𝐹:ω⟶dom 𝑥 ↔ (𝐹 Fn ω ∧ ∀𝑛 ∈ ω (𝐹‘𝑛) ∈ dom 𝑥)) |
55 | 5, 53, 54 | sylanbrc 585 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹:ω⟶dom 𝑥) |
56 | | omex 9100 |
. . . . . 6
⊢ ω
∈ V |
57 | 56 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ω ∈ V) |
58 | | vex 3498 |
. . . . . . 7
⊢ 𝑥 ∈ V |
59 | 58 | dmex 7610 |
. . . . . 6
⊢ dom 𝑥 ∈ V |
60 | 59 | a1i 11 |
. . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → dom 𝑥 ∈ V) |
61 | | fex2 7632 |
. . . . 5
⊢ ((𝐹:ω⟶dom 𝑥 ∧ ω ∈ V ∧
dom 𝑥 ∈ V) →
𝐹 ∈
V) |
62 | 55, 57, 60, 61 | syl3anc 1367 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 ∈ V) |
63 | 48 | ralrimiv 3181 |
. . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛)) |
64 | | fveq1 6664 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛)) |
65 | | fveq1 6664 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘suc 𝑛) = (𝐹‘suc 𝑛)) |
66 | 64, 65 | breq12d 5072 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
67 | 66 | ralbidv 3197 |
. . . 4
⊢ (𝑓 = 𝐹 → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) |
68 | 62, 63, 67 | spcedv 3599 |
. . 3
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
69 | 68 | 3exp 1115 |
. 2
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)))) |
70 | 59 | pwex 5274 |
. . 3
⊢ 𝒫
dom 𝑥 ∈
V |
71 | 70 | ac4c 9892 |
. 2
⊢
∃𝑔∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) |
72 | 69, 71 | exlimiiv 1928 |
1
⊢
(∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |