Proof of Theorem zfrep6
Step | Hyp | Ref
| Expression |
1 | | euex 2494 |
. . . . . . 7
⊢
(∃!𝑦𝜑 → ∃𝑦𝜑) |
2 | 1 | ralimi 2952 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∀𝑥 ∈ 𝑧 ∃𝑦𝜑) |
3 | | rabid2 3118 |
. . . . . 6
⊢ (𝑧 = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥 ∈ 𝑧 ∃𝑦𝜑) |
4 | 2, 3 | sylibr 224 |
. . . . 5
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → 𝑧 = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑}) |
5 | | 19.42v 1918 |
. . . . . . 7
⊢
(∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)) |
6 | 5 | abbii 2739 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)} |
7 | | dmopab 5335 |
. . . . . 6
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)} |
8 | | df-rab 2921 |
. . . . . 6
⊢ {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)} |
9 | 6, 7, 8 | 3eqtr4i 2654 |
. . . . 5
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} |
10 | 4, 9 | syl6reqr 2675 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = 𝑧) |
11 | | vex 3203 |
. . . 4
⊢ 𝑧 ∈ V |
12 | 10, 11 | syl6eqel 2709 |
. . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V) |
13 | | eumo 2499 |
. . . . . . 7
⊢
(∃!𝑦𝜑 → ∃*𝑦𝜑) |
14 | 13 | imim2i 16 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → (𝑥 ∈ 𝑧 → ∃*𝑦𝜑)) |
15 | | moanimv 2531 |
. . . . . 6
⊢
(∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 → ∃*𝑦𝜑)) |
16 | 14, 15 | sylibr 224 |
. . . . 5
⊢ ((𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
17 | 16 | alimi 1739 |
. . . 4
⊢
(∀𝑥(𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
18 | | df-ral 2917 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝑧 → ∃!𝑦𝜑)) |
19 | | funopab 5923 |
. . . 4
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
20 | 17, 18, 19 | 3imtr4i 281 |
. . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) |
21 | | funrnex 7133 |
. . 3
⊢ (dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V → (Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V)) |
22 | 12, 20, 21 | sylc 65 |
. 2
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V) |
23 | | nfra1 2941 |
. . 3
⊢
Ⅎ𝑥∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 |
24 | 10 | eleq2d 2687 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ 𝑥 ∈ 𝑧)) |
25 | | opabid 4982 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
26 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
27 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
28 | 26, 27 | opelrn 5357 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → 𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) |
29 | 25, 28 | sylbir 225 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → 𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) |
30 | 29 | ex 450 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑧 → (𝜑 → 𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)})) |
31 | 30 | impac 651 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → (𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) |
32 | 31 | eximi 1762 |
. . . . 5
⊢
(∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) → ∃𝑦(𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) |
33 | 7 | abeq2i 2735 |
. . . . 5
⊢ (𝑥 ∈ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
34 | | df-rex 2918 |
. . . . 5
⊢
(∃𝑦 ∈ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) |
35 | 32, 33, 34 | 3imtr4i 281 |
. . . 4
⊢ (𝑥 ∈ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑) |
36 | 24, 35 | syl6bir 244 |
. . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → (𝑥 ∈ 𝑧 → ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) |
37 | 23, 36 | ralrimi 2957 |
. 2
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑) |
38 | | nfopab1 4719 |
. . . . . 6
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
39 | 38 | nfrn 5368 |
. . . . 5
⊢
Ⅎ𝑥ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
40 | 39 | nfeq2 2780 |
. . . 4
⊢
Ⅎ𝑥 𝑤 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
41 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑦𝑤 |
42 | | nfopab2 4720 |
. . . . . 6
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
43 | 42 | nfrn 5368 |
. . . . 5
⊢
Ⅎ𝑦ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
44 | 41, 43 | rexeqf 3135 |
. . . 4
⊢ (𝑤 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → (∃𝑦 ∈ 𝑤 𝜑 ↔ ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) |
45 | 40, 44 | ralbid 2983 |
. . 3
⊢ (𝑤 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → (∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) |
46 | 45 | spcegv 3294 |
. 2
⊢ (ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V → (∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)) |
47 | 22, 37, 46 | sylc 65 |
1
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) |