Step | Hyp | Ref
| Expression |
1 | | neeq1 2996 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑦 ≠ ∅ ↔ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ≠ ∅)) |
2 | | abn0 4269 |
. . . . . . 7
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ≠ ∅ ↔ ∃𝑧(𝐹‘𝐾)𝑥𝑧) |
3 | 1, 2 | bitrdi 290 |
. . . . . 6
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑦 ≠ ∅ ↔ ∃𝑧(𝐹‘𝐾)𝑥𝑧)) |
4 | | eleq2 2821 |
. . . . . . . . 9
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝑦) ∈ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
5 | | breq2 5034 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → ((𝐹‘𝐾)𝑥𝑤 ↔ (𝐹‘𝐾)𝑥𝑧)) |
6 | 5 | cbvabv 2806 |
. . . . . . . . . 10
⊢ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} |
7 | 6 | eleq2i 2824 |
. . . . . . . . 9
⊢ ((𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} ↔ (𝑔‘𝑦) ∈ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
8 | 4, 7 | bitr4di 292 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤})) |
9 | | fvex 6689 |
. . . . . . . . 9
⊢ (𝑔‘𝑦) ∈ V |
10 | | breq2 5034 |
. . . . . . . . 9
⊢ (𝑤 = (𝑔‘𝑦) → ((𝐹‘𝐾)𝑥𝑤 ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦))) |
11 | 9, 10 | elab 3573 |
. . . . . . . 8
⊢ ((𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦)) |
12 | 8, 11 | bitrdi 290 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦))) |
13 | | fveq2 6676 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑔‘𝑦) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
14 | 13 | breq2d 5042 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝐹‘𝐾)𝑥(𝑔‘𝑦) ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
15 | 12, 14 | bitrd 282 |
. . . . . 6
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
16 | 3, 15 | imbi12d 348 |
. . . . 5
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ↔ (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
17 | 16 | rspcv 3521 |
. . . 4
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
18 | | fvex 6689 |
. . . . . . . 8
⊢ (𝐹‘𝐾) ∈ V |
19 | | vex 3402 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
20 | 18, 19 | brelrn 5785 |
. . . . . . 7
⊢ ((𝐹‘𝐾)𝑥𝑧 → 𝑧 ∈ ran 𝑥) |
21 | 20 | abssi 3959 |
. . . . . 6
⊢ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ ran 𝑥 |
22 | | sstr 3885 |
. . . . . 6
⊢ (({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ ran 𝑥 ∧ ran 𝑥 ⊆ dom 𝑥) → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
23 | 21, 22 | mpan 690 |
. . . . 5
⊢ (ran
𝑥 ⊆ dom 𝑥 → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
24 | | vex 3402 |
. . . . . . 7
⊢ 𝑥 ∈ V |
25 | 24 | dmex 7644 |
. . . . . 6
⊢ dom 𝑥 ∈ V |
26 | 25 | elpw2 5213 |
. . . . 5
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥 ↔ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
27 | 23, 26 | sylibr 237 |
. . . 4
⊢ (ran
𝑥 ⊆ dom 𝑥 → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥) |
28 | 17, 27 | syl11 33 |
. . 3
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (ran 𝑥 ⊆ dom 𝑥 → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
29 | 28 | 3imp 1112 |
. 2
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘𝐾)𝑥𝑧) → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
30 | | fvex 6689 |
. . . 4
⊢ (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) ∈ V |
31 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑦𝑠 |
32 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑦𝐾 |
33 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑦(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
34 | | axdclem.1 |
. . . . 5
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
35 | | breq1 5033 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐾) → (𝑦𝑥𝑧 ↔ (𝐹‘𝐾)𝑥𝑧)) |
36 | 35 | abbidv 2802 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐾) → {𝑧 ∣ 𝑦𝑥𝑧} = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
37 | 36 | fveq2d 6680 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐾) → (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧}) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
38 | 31, 32, 33, 34, 37 | frsucmpt 8104 |
. . . 4
⊢ ((𝐾 ∈ ω ∧ (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) ∈ V) → (𝐹‘suc 𝐾) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
39 | 30, 38 | mpan2 691 |
. . 3
⊢ (𝐾 ∈ ω → (𝐹‘suc 𝐾) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
40 | 39 | breq2d 5042 |
. 2
⊢ (𝐾 ∈ ω → ((𝐹‘𝐾)𝑥(𝐹‘suc 𝐾) ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
41 | 29, 40 | syl5ibrcom 250 |
1
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘𝐾)𝑥𝑧) → (𝐾 ∈ ω → (𝐹‘𝐾)𝑥(𝐹‘suc 𝐾))) |