Step | Hyp | Ref
| Expression |
1 | | funopab 6384 |
. . . 4
⊢ (Fun
{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ↔ ∀𝑤∃*𝑧∀𝑦𝜑) |
2 | | nfa1 2156 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑦𝜑 |
3 | 2 | mof 2564 |
. . . . 5
⊢
(∃*𝑧∀𝑦𝜑 ↔ ∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦)) |
4 | 3 | albii 1826 |
. . . 4
⊢
(∀𝑤∃*𝑧∀𝑦𝜑 ↔ ∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦)) |
5 | 1, 4 | bitr2i 279 |
. . 3
⊢
(∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) ↔ Fun {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
6 | | vex 3404 |
. . . . . . 7
⊢ 𝑥 ∈ V |
7 | | eleq2w2 2735 |
. . . . . . 7
⊢ (Fin = V
→ (𝑥 ∈ Fin ↔
𝑥 ∈
V)) |
8 | 6, 7 | mpbiri 261 |
. . . . . 6
⊢ (Fin = V
→ 𝑥 ∈
Fin) |
9 | | imafi 8785 |
. . . . . 6
⊢ ((Fun
{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ∧ 𝑥 ∈ Fin) → ({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) ∈ Fin) |
10 | 8, 9 | sylan2 596 |
. . . . 5
⊢ ((Fun
{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ∧ Fin = V) → ({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) ∈ Fin) |
11 | 10 | elexd 3420 |
. . . 4
⊢ ((Fun
{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ∧ Fin = V) → ({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) ∈ V) |
12 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑤 ∈ 𝑥 |
13 | 2 | nfopab 5108 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} |
14 | 13 | nfel2 2918 |
. . . . . . . . . 10
⊢
Ⅎ𝑦〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} |
15 | 12, 14 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
16 | 15 | nfex 2327 |
. . . . . . . 8
⊢
Ⅎ𝑦∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
17 | 16 | nfab 2906 |
. . . . . . 7
⊢
Ⅎ𝑦{𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} |
18 | 17 | issetf 3414 |
. . . . . 6
⊢ ({𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} ∈ V ↔ ∃𝑦 𝑦 = {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})}) |
19 | | abeq2 2865 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}))) |
20 | 19 | exbii 1854 |
. . . . . 6
⊢
(∃𝑦 𝑦 = {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}))) |
21 | | opabidw 5390 |
. . . . . . . . . . 11
⊢
(〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ↔ ∀𝑦𝜑) |
22 | 21 | anbi2i 626 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)) |
23 | 22 | exbii 1854 |
. . . . . . . . 9
⊢
(∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)) |
24 | 23 | bibi2i 341 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})) ↔ (𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
25 | 24 | albii 1826 |
. . . . . . 7
⊢
(∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
26 | 25 | exbii 1854 |
. . . . . 6
⊢
(∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
27 | 18, 20, 26 | 3bitrri 301 |
. . . . 5
⊢
(∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)) ↔ {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} ∈ V) |
28 | | dfima3 5916 |
. . . . . . 7
⊢
({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) = {𝑣 ∣ ∃𝑢(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} |
29 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑧 𝑢 ∈ 𝑥 |
30 | | nfopab2 5110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} |
31 | 30 | nfel2 2918 |
. . . . . . . . . 10
⊢
Ⅎ𝑧〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} |
32 | 29, 31 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑧(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
33 | 32 | nfex 2327 |
. . . . . . . 8
⊢
Ⅎ𝑧∃𝑢(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
34 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑣∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
35 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤 𝑢 ∈ 𝑥 |
36 | | nfopab1 5109 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑤{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} |
37 | 36 | nfel2 2918 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} |
38 | 35, 37 | nfan 1906 |
. . . . . . . . . 10
⊢
Ⅎ𝑤(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
39 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑢(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) |
40 | | elequ1 2121 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → (𝑢 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
41 | | opeq1 4769 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → 〈𝑢, 𝑣〉 = 〈𝑤, 𝑣〉) |
42 | 41 | eleq1d 2818 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → (〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ↔ 〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})) |
43 | 40, 42 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → ((𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ (𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}))) |
44 | 38, 39, 43 | cbvexv1 2345 |
. . . . . . . . 9
⊢
(∃𝑢(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})) |
45 | | opeq2 4771 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑧 → 〈𝑤, 𝑣〉 = 〈𝑤, 𝑧〉) |
46 | 45 | eleq1d 2818 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑧 → (〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ↔ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})) |
47 | 46 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑧 → ((𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ (𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}))) |
48 | 47 | exbidv 1928 |
. . . . . . . . 9
⊢ (𝑣 = 𝑧 → (∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}))) |
49 | 44, 48 | syl5bb 286 |
. . . . . . . 8
⊢ (𝑣 = 𝑧 → (∃𝑢(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑}))) |
50 | 33, 34, 49 | cbvabw 2808 |
. . . . . . 7
⊢ {𝑣 ∣ ∃𝑢(𝑢 ∈ 𝑥 ∧ 〈𝑢, 𝑣〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} = {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} |
51 | 28, 50 | eqtri 2762 |
. . . . . 6
⊢
({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) = {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} |
52 | 51 | eleq1i 2824 |
. . . . 5
⊢
(({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) ∈ V ↔ {𝑧 ∣ ∃𝑤(𝑤 ∈ 𝑥 ∧ 〈𝑤, 𝑧〉 ∈ {〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑})} ∈ V) |
53 | 27, 52 | bitr4i 281 |
. . . 4
⊢
(∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)) ↔ ({〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} “ 𝑥) ∈ V) |
54 | 11, 53 | sylibr 237 |
. . 3
⊢ ((Fun
{〈𝑤, 𝑧〉 ∣ ∀𝑦𝜑} ∧ Fin = V) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
55 | 5, 54 | sylanb 584 |
. 2
⊢
((∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) ∧ Fin = V) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
56 | 55 | expcom 417 |
1
⊢ (Fin = V
→ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))) |