| Step | Hyp | Ref
| Expression |
| 1 | | neeq1 3003 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑦 ≠ ∅ ↔ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ≠ ∅)) |
| 2 | | abn0 4385 |
. . . . . . 7
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ≠ ∅ ↔ ∃𝑧(𝐹‘𝐾)𝑥𝑧) |
| 3 | 1, 2 | bitrdi 287 |
. . . . . 6
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑦 ≠ ∅ ↔ ∃𝑧(𝐹‘𝐾)𝑥𝑧)) |
| 4 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝑦) ∈ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
| 5 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → ((𝐹‘𝐾)𝑥𝑤 ↔ (𝐹‘𝐾)𝑥𝑧)) |
| 6 | 5 | cbvabv 2812 |
. . . . . . . . . 10
⊢ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} |
| 7 | 6 | eleq2i 2833 |
. . . . . . . . 9
⊢ ((𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} ↔ (𝑔‘𝑦) ∈ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
| 8 | 4, 7 | bitr4di 289 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤})) |
| 9 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑔‘𝑦) ∈ V |
| 10 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑤 = (𝑔‘𝑦) → ((𝐹‘𝐾)𝑥𝑤 ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦))) |
| 11 | 9, 10 | elab 3679 |
. . . . . . . 8
⊢ ((𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦)) |
| 12 | 8, 11 | bitrdi 287 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦))) |
| 13 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑔‘𝑦) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
| 14 | 13 | breq2d 5155 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝐹‘𝐾)𝑥(𝑔‘𝑦) ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
| 15 | 12, 14 | bitrd 279 |
. . . . . 6
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
| 16 | 3, 15 | imbi12d 344 |
. . . . 5
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ↔ (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
| 17 | 16 | rspcv 3618 |
. . . 4
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
| 18 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘𝐾) ∈ V |
| 19 | | vex 3484 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
| 20 | 18, 19 | brelrn 5953 |
. . . . . . 7
⊢ ((𝐹‘𝐾)𝑥𝑧 → 𝑧 ∈ ran 𝑥) |
| 21 | 20 | abssi 4070 |
. . . . . 6
⊢ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ ran 𝑥 |
| 22 | | sstr 3992 |
. . . . . 6
⊢ (({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ ran 𝑥 ∧ ran 𝑥 ⊆ dom 𝑥) → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
| 23 | 21, 22 | mpan 690 |
. . . . 5
⊢ (ran
𝑥 ⊆ dom 𝑥 → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
| 24 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 25 | 24 | dmex 7931 |
. . . . . 6
⊢ dom 𝑥 ∈ V |
| 26 | 25 | elpw2 5334 |
. . . . 5
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥 ↔ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
| 27 | 23, 26 | sylibr 234 |
. . . 4
⊢ (ran
𝑥 ⊆ dom 𝑥 → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥) |
| 28 | 17, 27 | syl11 33 |
. . 3
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (ran 𝑥 ⊆ dom 𝑥 → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
| 29 | 28 | 3imp 1111 |
. 2
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘𝐾)𝑥𝑧) → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
| 30 | | fvex 6919 |
. . . 4
⊢ (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) ∈ V |
| 31 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦𝑠 |
| 32 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦𝐾 |
| 33 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
| 34 | | axdclem.1 |
. . . . 5
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
| 35 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐾) → (𝑦𝑥𝑧 ↔ (𝐹‘𝐾)𝑥𝑧)) |
| 36 | 35 | abbidv 2808 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐾) → {𝑧 ∣ 𝑦𝑥𝑧} = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
| 37 | 36 | fveq2d 6910 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐾) → (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧}) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
| 38 | 31, 32, 33, 34, 37 | frsucmpt 8478 |
. . . 4
⊢ ((𝐾 ∈ ω ∧ (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) ∈ V) → (𝐹‘suc 𝐾) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
| 39 | 30, 38 | mpan2 691 |
. . 3
⊢ (𝐾 ∈ ω → (𝐹‘suc 𝐾) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
| 40 | 39 | breq2d 5155 |
. 2
⊢ (𝐾 ∈ ω → ((𝐹‘𝐾)𝑥(𝐹‘suc 𝐾) ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
| 41 | 29, 40 | syl5ibrcom 247 |
1
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘𝐾)𝑥𝑧) → (𝐾 ∈ ω → (𝐹‘𝐾)𝑥(𝐹‘suc 𝐾))) |