Proof of Theorem zfrep6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 19.42v 1952 | . . . . . . 7
⊢
(∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)) | 
| 2 | 1 | abbii 2808 | . . . . . 6
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)} | 
| 3 |  | dmopab 5925 | . . . . . 6
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)} | 
| 4 |  | df-rab 3436 | . . . . . 6
⊢ {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)} | 
| 5 | 2, 3, 4 | 3eqtr4i 2774 | . . . . 5
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} | 
| 6 |  | euex 2576 | . . . . . . 7
⊢
(∃!𝑦𝜑 → ∃𝑦𝜑) | 
| 7 | 6 | ralimi 3082 | . . . . . 6
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∀𝑥 ∈ 𝑧 ∃𝑦𝜑) | 
| 8 |  | rabid2 3469 | . . . . . 6
⊢ (𝑧 = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥 ∈ 𝑧 ∃𝑦𝜑) | 
| 9 | 7, 8 | sylibr 234 | . . . . 5
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → 𝑧 = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑}) | 
| 10 | 5, 9 | eqtr4id 2795 | . . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = 𝑧) | 
| 11 |  | vex 3483 | . . . 4
⊢ 𝑧 ∈ V | 
| 12 | 10, 11 | eqeltrdi 2848 | . . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V) | 
| 13 |  | eumo 2577 | . . . . . . 7
⊢
(∃!𝑦𝜑 → ∃*𝑦𝜑) | 
| 14 | 13 | imim2i 16 | . . . . . 6
⊢ ((𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → (𝑥 ∈ 𝑧 → ∃*𝑦𝜑)) | 
| 15 |  | moanimv 2618 | . . . . . 6
⊢
(∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 → ∃*𝑦𝜑)) | 
| 16 | 14, 15 | sylibr 234 | . . . . 5
⊢ ((𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) | 
| 17 | 16 | alimi 1810 | . . . 4
⊢
(∀𝑥(𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) | 
| 18 |  | df-ral 3061 | . . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝑧 → ∃!𝑦𝜑)) | 
| 19 |  | funopab 6600 | . . . 4
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) | 
| 20 | 17, 18, 19 | 3imtr4i 292 | . . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) | 
| 21 |  | funrnex 7979 | . . 3
⊢ (dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V → (Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V)) | 
| 22 | 12, 20, 21 | sylc 65 | . 2
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V) | 
| 23 |  | nfra1 3283 | . . 3
⊢
Ⅎ𝑥∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 | 
| 24 | 10 | eleq2d 2826 | . . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ 𝑥 ∈ 𝑧)) | 
| 25 |  | opabidw 5528 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | 
| 26 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑥 ∈ V | 
| 27 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 28 | 26, 27 | opelrn 5953 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → 𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) | 
| 29 | 25, 28 | sylbir 235 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → 𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) | 
| 30 | 29 | ex 412 | . . . . . . 7
⊢ (𝑥 ∈ 𝑧 → (𝜑 → 𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)})) | 
| 31 | 30 | impac 552 | . . . . . 6
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → (𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) | 
| 32 | 31 | eximi 1834 | . . . . 5
⊢
(∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) → ∃𝑦(𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) | 
| 33 | 3 | eqabri 2884 | . . . . 5
⊢ (𝑥 ∈ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) | 
| 34 |  | df-rex 3070 | . . . . 5
⊢
(∃𝑦 ∈ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) | 
| 35 | 32, 33, 34 | 3imtr4i 292 | . . . 4
⊢ (𝑥 ∈ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑) | 
| 36 | 24, 35 | biimtrrdi 254 | . . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → (𝑥 ∈ 𝑧 → ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) | 
| 37 | 23, 36 | ralrimi 3256 | . 2
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑) | 
| 38 |  | nfopab1 5212 | . . . . 5
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} | 
| 39 | 38 | nfrn 5962 | . . . 4
⊢
Ⅎ𝑥ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} | 
| 40 | 39 | nfeq2 2922 | . . 3
⊢
Ⅎ𝑥 𝑤 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} | 
| 41 |  | nfcv 2904 | . . . 4
⊢
Ⅎ𝑦𝑤 | 
| 42 |  | nfopab2 5213 | . . . . 5
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} | 
| 43 | 42 | nfrn 5962 | . . . 4
⊢
Ⅎ𝑦ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} | 
| 44 | 41, 43 | rexeqf 3353 | . . 3
⊢ (𝑤 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → (∃𝑦 ∈ 𝑤 𝜑 ↔ ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) | 
| 45 | 40, 44 | ralbid 3272 | . 2
⊢ (𝑤 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → (∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) | 
| 46 | 22, 37, 45 | spcedv 3597 | 1
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) |