| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frfnom 8476 | . . . . . . 7
⊢
(rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω | 
| 2 |  | axdclem2.1 | . . . . . . . 8
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) | 
| 3 | 2 | fneq1i 6664 | . . . . . . 7
⊢ (𝐹 Fn ω ↔ (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn
ω) | 
| 4 | 1, 3 | mpbir 231 | . . . . . 6
⊢ 𝐹 Fn ω | 
| 5 | 4 | a1i 11 | . . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 Fn ω) | 
| 6 |  | omex 9684 | . . . . . 6
⊢ ω
∈ V | 
| 7 | 6 | a1i 11 | . . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ω ∈ V) | 
| 8 | 5, 7 | fnexd 7239 | . . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 ∈ V) | 
| 9 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑛 = ∅ → (𝐹‘𝑛) = (𝐹‘∅)) | 
| 10 |  | suceq 6449 | . . . . . . . . 9
⊢ (𝑛 = ∅ → suc 𝑛 = suc ∅) | 
| 11 | 10 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑛 = ∅ → (𝐹‘suc 𝑛) = (𝐹‘suc ∅)) | 
| 12 | 9, 11 | breq12d 5155 | . . . . . . 7
⊢ (𝑛 = ∅ → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘∅)𝑥(𝐹‘suc ∅))) | 
| 13 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) | 
| 14 |  | suceq 6449 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘) | 
| 15 | 14 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc 𝑘)) | 
| 16 | 13, 15 | breq12d 5155 | . . . . . . 7
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘𝑘)𝑥(𝐹‘suc 𝑘))) | 
| 17 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑛 = suc 𝑘 → (𝐹‘𝑛) = (𝐹‘suc 𝑘)) | 
| 18 |  | suceq 6449 | . . . . . . . . 9
⊢ (𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘) | 
| 19 | 18 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑛 = suc 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc suc 𝑘)) | 
| 20 | 17, 19 | breq12d 5155 | . . . . . . 7
⊢ (𝑛 = suc 𝑘 → ((𝐹‘𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) | 
| 21 | 2 | fveq1i 6906 | . . . . . . . . . . . . 13
⊢ (𝐹‘∅) = ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾
ω)‘∅) | 
| 22 |  | fr0g 8477 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ V → ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠) | 
| 23 | 22 | elv 3484 | . . . . . . . . . . . . 13
⊢
((rec((𝑦 ∈ V
↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠 | 
| 24 | 21, 23 | eqtri 2764 | . . . . . . . . . . . 12
⊢ (𝐹‘∅) = 𝑠 | 
| 25 | 24 | breq1i 5149 | . . . . . . . . . . 11
⊢ ((𝐹‘∅)𝑥𝑧 ↔ 𝑠𝑥𝑧) | 
| 26 | 25 | biimpri 228 | . . . . . . . . . 10
⊢ (𝑠𝑥𝑧 → (𝐹‘∅)𝑥𝑧) | 
| 27 | 26 | eximi 1834 | . . . . . . . . 9
⊢
(∃𝑧 𝑠𝑥𝑧 → ∃𝑧(𝐹‘∅)𝑥𝑧) | 
| 28 |  | peano1 7911 | . . . . . . . . . 10
⊢ ∅
∈ ω | 
| 29 | 2 | axdclem 10560 | . . . . . . . . . 10
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (∅ ∈ ω →
(𝐹‘∅)𝑥(𝐹‘suc ∅))) | 
| 30 | 28, 29 | mpi 20 | . . . . . . . . 9
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) | 
| 31 | 27, 30 | syl3an3 1165 | . . . . . . . 8
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧 𝑠𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) | 
| 32 | 31 | 3com23 1126 | . . . . . . 7
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘∅)𝑥(𝐹‘suc ∅)) | 
| 33 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝐹‘𝑘) ∈ V | 
| 34 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢ (𝐹‘suc 𝑘) ∈ V | 
| 35 | 33, 34 | brelrn 5952 | . . . . . . . . . . . . 13
⊢ ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ ran 𝑥) | 
| 36 |  | ssel 3976 | . . . . . . . . . . . . 13
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘suc 𝑘) ∈ ran 𝑥 → (𝐹‘suc 𝑘) ∈ dom 𝑥)) | 
| 37 | 35, 36 | syl5 34 | . . . . . . . . . . . 12
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ dom 𝑥)) | 
| 38 | 34 | eldm 5910 | . . . . . . . . . . . 12
⊢ ((𝐹‘suc 𝑘) ∈ dom 𝑥 ↔ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) | 
| 39 | 37, 38 | imbitrdi 251 | . . . . . . . . . . 11
⊢ (ran
𝑥 ⊆ dom 𝑥 → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) | 
| 40 | 39 | ad2antll 729 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)) | 
| 41 |  | peano2 7913 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) | 
| 42 | 2 | axdclem 10560 | . . . . . . . . . . . . . 14
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (suc 𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) | 
| 43 | 41, 42 | syl5 34 | . . . . . . . . . . . . 13
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) | 
| 44 | 43 | 3expia 1121 | . . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) | 
| 45 | 44 | com3r 87 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) | 
| 46 | 45 | imp 406 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) | 
| 47 | 40, 46 | syld 47 | . . . . . . . . 9
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) | 
| 48 | 47 | 3adantr2 1170 | . . . . . . . 8
⊢ ((𝑘 ∈ ω ∧
(∀𝑦 ∈ 𝒫
dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))) | 
| 49 | 48 | ex 412 | . . . . . . 7
⊢ (𝑘 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ((𝐹‘𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))) | 
| 50 | 12, 16, 20, 32, 49 | finds2 7921 | . . . . . 6
⊢ (𝑛 ∈ ω →
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) | 
| 51 | 50 | com12 32 | . . . . 5
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) | 
| 52 | 51 | ralrimiv 3144 | . . . 4
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛)) | 
| 53 |  | fveq1 6904 | . . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛)) | 
| 54 |  | fveq1 6904 | . . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘suc 𝑛) = (𝐹‘suc 𝑛)) | 
| 55 | 53, 54 | breq12d 5155 | . . . . 5
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) | 
| 56 | 55 | ralbidv 3177 | . . . 4
⊢ (𝑓 = 𝐹 → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛)𝑥(𝐹‘suc 𝑛))) | 
| 57 | 8, 52, 56 | spcedv 3597 | . . 3
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) | 
| 58 | 57 | 3exp 1119 | . 2
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)))) | 
| 59 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 60 | 59 | dmex 7932 | . . . 4
⊢ dom 𝑥 ∈ V | 
| 61 | 60 | pwex 5379 | . . 3
⊢ 𝒫
dom 𝑥 ∈
V | 
| 62 | 61 | ac4c 10517 | . 2
⊢
∃𝑔∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) | 
| 63 | 58, 62 | exlimiiv 1930 | 1
⊢
(∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |