Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐹‘𝐾) ∈ V |
2 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
3 | 1, 2 | brelrn 5277 |
. . . . . . . 8
⊢ ((𝐹‘𝐾)𝑥𝑧 → 𝑧 ∈ ran 𝑥) |
4 | 3 | abssi 3640 |
. . . . . . 7
⊢ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ ran 𝑥 |
5 | | sstr 3576 |
. . . . . . 7
⊢ (({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ ran 𝑥 ∧ ran 𝑥 ⊆ dom 𝑥) → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
6 | 4, 5 | mpan 702 |
. . . . . 6
⊢ (ran
𝑥 ⊆ dom 𝑥 → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
7 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
8 | 7 | dmex 6991 |
. . . . . . 7
⊢ dom 𝑥 ∈ V |
9 | 8 | elpw2 4755 |
. . . . . 6
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥 ↔ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ⊆ dom 𝑥) |
10 | 6, 9 | sylibr 223 |
. . . . 5
⊢ (ran
𝑥 ⊆ dom 𝑥 → {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥) |
11 | | neeq1 2844 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑦 ≠ ∅ ↔ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ≠ ∅)) |
12 | | abn0 3908 |
. . . . . . . 8
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ≠ ∅ ↔ ∃𝑧(𝐹‘𝐾)𝑥𝑧) |
13 | 11, 12 | syl6bb 275 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑦 ≠ ∅ ↔ ∃𝑧(𝐹‘𝐾)𝑥𝑧)) |
14 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝑦) ∈ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
15 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → ((𝐹‘𝐾)𝑥𝑤 ↔ (𝐹‘𝐾)𝑥𝑧)) |
16 | 15 | cbvabv 2734 |
. . . . . . . . . . 11
⊢ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} |
17 | 16 | eleq2i 2680 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} ↔ (𝑔‘𝑦) ∈ {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
18 | 14, 17 | syl6bbr 277 |
. . . . . . . . 9
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤})) |
19 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑔‘𝑦) ∈ V |
20 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑔‘𝑦) → ((𝐹‘𝐾)𝑥𝑤 ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦))) |
21 | 19, 20 | elab 3319 |
. . . . . . . . 9
⊢ ((𝑔‘𝑦) ∈ {𝑤 ∣ (𝐹‘𝐾)𝑥𝑤} ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦)) |
22 | 18, 21 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝐹‘𝐾)𝑥(𝑔‘𝑦))) |
23 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → (𝑔‘𝑦) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
24 | 23 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝐹‘𝐾)𝑥(𝑔‘𝑦) ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
25 | 22, 24 | bitrd 267 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
26 | 13, 25 | imbi12d 333 |
. . . . . 6
⊢ (𝑦 = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} → ((𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ↔ (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
27 | 26 | rspcv 3278 |
. . . . 5
⊢ ({𝑧 ∣ (𝐹‘𝐾)𝑥𝑧} ∈ 𝒫 dom 𝑥 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
28 | 10, 27 | syl 17 |
. . . 4
⊢ (ran
𝑥 ⊆ dom 𝑥 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
29 | 28 | com12 32 |
. . 3
⊢
(∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (ran 𝑥 ⊆ dom 𝑥 → (∃𝑧(𝐹‘𝐾)𝑥𝑧 → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})))) |
30 | 29 | 3imp 1249 |
. 2
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘𝐾)𝑥𝑧) → (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
31 | | fvex 6113 |
. . . 4
⊢ (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) ∈ V |
32 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦𝑠 |
33 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦𝐾 |
34 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
35 | | axdclem.1 |
. . . . 5
⊢ 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧})), 𝑠) ↾ ω) |
36 | | breq1 4586 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐾) → (𝑦𝑥𝑧 ↔ (𝐹‘𝐾)𝑥𝑧)) |
37 | 36 | abbidv 2728 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐾) → {𝑧 ∣ 𝑦𝑥𝑧} = {𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) |
38 | 37 | fveq2d 6107 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐾) → (𝑔‘{𝑧 ∣ 𝑦𝑥𝑧}) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
39 | 32, 33, 34, 35, 38 | frsucmpt 7420 |
. . . 4
⊢ ((𝐾 ∈ ω ∧ (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}) ∈ V) → (𝐹‘suc 𝐾) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
40 | 31, 39 | mpan2 703 |
. . 3
⊢ (𝐾 ∈ ω → (𝐹‘suc 𝐾) = (𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧})) |
41 | 40 | breq2d 4595 |
. 2
⊢ (𝐾 ∈ ω → ((𝐹‘𝐾)𝑥(𝐹‘suc 𝐾) ↔ (𝐹‘𝐾)𝑥(𝑔‘{𝑧 ∣ (𝐹‘𝐾)𝑥𝑧}))) |
42 | 30, 41 | syl5ibrcom 236 |
1
⊢
((∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘𝐾)𝑥𝑧) → (𝐾 ∈ ω → (𝐹‘𝐾)𝑥(𝐹‘suc 𝐾))) |