Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . 6
⊢ 𝑦 ∈ V |
2 | 1 | rnex 7100 |
. . . . 5
⊢ ran 𝑦 ∈ V |
3 | 2 | pwex 4848 |
. . . 4
⊢ 𝒫
ran 𝑦 ∈
V |
4 | | raleq 3138 |
. . . . 5
⊢ (𝑥 = 𝒫 ran 𝑦 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
5 | 4 | exbidv 1850 |
. . . 4
⊢ (𝑥 = 𝒫 ran 𝑦 → (∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ 𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
6 | 3, 5 | spcv 3299 |
. . 3
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓∀𝑧 ∈ 𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
7 | | aceq3lem.1 |
. . . . . . 7
⊢ 𝐹 = (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
8 | | df-mpt 4730 |
. . . . . . 7
⊢ (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) = {〈𝑤, ℎ〉 ∣ (𝑤 ∈ dom 𝑦 ∧ ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))} |
9 | 7, 8 | eqtri 2644 |
. . . . . 6
⊢ 𝐹 = {〈𝑤, ℎ〉 ∣ (𝑤 ∈ dom 𝑦 ∧ ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))} |
10 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
11 | 10 | eldm 5321 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ dom 𝑦 ↔ ∃𝑢 𝑤𝑦𝑢) |
12 | | abn0 3954 |
. . . . . . . . . . . . . 14
⊢ ({𝑢 ∣ 𝑤𝑦𝑢} ≠ ∅ ↔ ∃𝑢 𝑤𝑦𝑢) |
13 | 11, 12 | bitr4i 267 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ dom 𝑦 ↔ {𝑢 ∣ 𝑤𝑦𝑢} ≠ ∅) |
14 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
15 | 10, 14 | brelrn 5356 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤𝑦𝑢 → 𝑢 ∈ ran 𝑦) |
16 | 15 | abssi 3677 |
. . . . . . . . . . . . . . 15
⊢ {𝑢 ∣ 𝑤𝑦𝑢} ⊆ ran 𝑦 |
17 | 2 | elpw2 4828 |
. . . . . . . . . . . . . . 15
⊢ ({𝑢 ∣ 𝑤𝑦𝑢} ∈ 𝒫 ran 𝑦 ↔ {𝑢 ∣ 𝑤𝑦𝑢} ⊆ ran 𝑦) |
18 | 16, 17 | mpbir 221 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∣ 𝑤𝑦𝑢} ∈ 𝒫 ran 𝑦 |
19 | | neeq1 2856 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = {𝑢 ∣ 𝑤𝑦𝑢} → (𝑧 ≠ ∅ ↔ {𝑢 ∣ 𝑤𝑦𝑢} ≠ ∅)) |
20 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = {𝑢 ∣ 𝑤𝑦𝑢} → (𝑓‘𝑧) = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
21 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = {𝑢 ∣ 𝑤𝑦𝑢} → 𝑧 = {𝑢 ∣ 𝑤𝑦𝑢}) |
22 | 20, 21 | eleq12d 2695 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = {𝑢 ∣ 𝑤𝑦𝑢} → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢})) |
23 | 19, 22 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = {𝑢 ∣ 𝑤𝑦𝑢} → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ({𝑢 ∣ 𝑤𝑦𝑢} ≠ ∅ → (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢}))) |
24 | 23 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢ ({𝑢 ∣ 𝑤𝑦𝑢} ∈ 𝒫 ran 𝑦 → (∀𝑧 ∈ 𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ({𝑢 ∣ 𝑤𝑦𝑢} ≠ ∅ → (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢}))) |
25 | 18, 24 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ({𝑢 ∣ 𝑤𝑦𝑢} ≠ ∅ → (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢})) |
26 | 13, 25 | syl5bi 232 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑤 ∈ dom 𝑦 → (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢})) |
27 | 26 | imp 445 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ dom 𝑦) → (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢}) |
28 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ V |
29 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) → (𝑤𝑦𝑧 ↔ 𝑤𝑦(𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))) |
30 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑧 → (𝑤𝑦𝑢 ↔ 𝑤𝑦𝑧)) |
31 | 30 | cbvabv 2747 |
. . . . . . . . . . . 12
⊢ {𝑢 ∣ 𝑤𝑦𝑢} = {𝑧 ∣ 𝑤𝑦𝑧} |
32 | 28, 29, 31 | elab2 3354 |
. . . . . . . . . . 11
⊢ ((𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) ∈ {𝑢 ∣ 𝑤𝑦𝑢} ↔ 𝑤𝑦(𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
33 | 27, 32 | sylib 208 |
. . . . . . . . . 10
⊢
((∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ dom 𝑦) → 𝑤𝑦(𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
34 | | breq2 4657 |
. . . . . . . . . 10
⊢ (ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) → (𝑤𝑦ℎ ↔ 𝑤𝑦(𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))) |
35 | 33, 34 | syl5ibrcom 237 |
. . . . . . . . 9
⊢
((∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ dom 𝑦) → (ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}) → 𝑤𝑦ℎ)) |
36 | 35 | expimpd 629 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑤 ∈ dom 𝑦 ∧ ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) → 𝑤𝑦ℎ)) |
37 | 36 | ssopab2dv 5004 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → {〈𝑤, ℎ〉 ∣ (𝑤 ∈ dom 𝑦 ∧ ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))} ⊆ {〈𝑤, ℎ〉 ∣ 𝑤𝑦ℎ}) |
38 | | opabss 4714 |
. . . . . . 7
⊢
{〈𝑤, ℎ〉 ∣ 𝑤𝑦ℎ} ⊆ 𝑦 |
39 | 37, 38 | syl6ss 3615 |
. . . . . 6
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → {〈𝑤, ℎ〉 ∣ (𝑤 ∈ dom 𝑦 ∧ ℎ = (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))} ⊆ 𝑦) |
40 | 9, 39 | syl5eqss 3649 |
. . . . 5
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → 𝐹 ⊆ 𝑦) |
41 | 28, 7 | fnmpti 6022 |
. . . . 5
⊢ 𝐹 Fn dom 𝑦 |
42 | 1 | ssex 4802 |
. . . . . . 7
⊢ (𝐹 ⊆ 𝑦 → 𝐹 ∈ V) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ ((𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦) → 𝐹 ∈ V) |
44 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (𝑔 ⊆ 𝑦 ↔ 𝐹 ⊆ 𝑦)) |
45 | | fneq1 5979 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (𝑔 Fn dom 𝑦 ↔ 𝐹 Fn dom 𝑦)) |
46 | 44, 45 | anbi12d 747 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ↔ (𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦))) |
47 | 46 | spcegv 3294 |
. . . . . 6
⊢ (𝐹 ∈ V → ((𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦) → ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))) |
48 | 43, 47 | mpcom 38 |
. . . . 5
⊢ ((𝐹 ⊆ 𝑦 ∧ 𝐹 Fn dom 𝑦) → ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)) |
49 | 40, 41, 48 | sylancl 694 |
. . . 4
⊢
(∀𝑧 ∈
𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)) |
50 | 49 | exlimiv 1858 |
. . 3
⊢
(∃𝑓∀𝑧 ∈ 𝒫 ran 𝑦(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)) |
51 | 6, 50 | syl 17 |
. 2
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)) |
52 | | sseq1 3626 |
. . . 4
⊢ (𝑔 = 𝑓 → (𝑔 ⊆ 𝑦 ↔ 𝑓 ⊆ 𝑦)) |
53 | | fneq1 5979 |
. . . 4
⊢ (𝑔 = 𝑓 → (𝑔 Fn dom 𝑦 ↔ 𝑓 Fn dom 𝑦)) |
54 | 52, 53 | anbi12d 747 |
. . 3
⊢ (𝑔 = 𝑓 → ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦))) |
55 | 54 | cbvexv 2275 |
. 2
⊢
(∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
56 | 51, 55 | sylib 208 |
1
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |