Step |
Hyp |
Ref |
Expression |
1 |
|
axgroth5 |
⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) |
2 |
|
biid |
⊢ ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) |
3 |
|
pweq |
⊢ ( 𝑧 = 𝑣 → 𝒫 𝑧 = 𝒫 𝑣 ) |
4 |
3
|
sseq1d |
⊢ ( 𝑧 = 𝑣 → ( 𝒫 𝑧 ⊆ 𝑦 ↔ 𝒫 𝑣 ⊆ 𝑦 ) ) |
5 |
4
|
cbvralvw |
⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ↔ ∀ 𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦 ) |
6 |
|
ssid |
⊢ 𝒫 𝑧 ⊆ 𝒫 𝑧 |
7 |
|
sseq2 |
⊢ ( 𝑤 = 𝒫 𝑧 → ( 𝒫 𝑧 ⊆ 𝑤 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑧 ) ) |
8 |
7
|
rspcev |
⊢ ( ( 𝒫 𝑧 ∈ 𝑦 ∧ 𝒫 𝑧 ⊆ 𝒫 𝑧 ) → ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) |
9 |
6 8
|
mpan2 |
⊢ ( 𝒫 𝑧 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) |
10 |
|
pweq |
⊢ ( 𝑣 = 𝑤 → 𝒫 𝑣 = 𝒫 𝑤 ) |
11 |
10
|
sseq1d |
⊢ ( 𝑣 = 𝑤 → ( 𝒫 𝑣 ⊆ 𝑦 ↔ 𝒫 𝑤 ⊆ 𝑦 ) ) |
12 |
11
|
rspccv |
⊢ ( ∀ 𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝒫 𝑤 ⊆ 𝑦 ) ) |
13 |
|
pwss |
⊢ ( 𝒫 𝑤 ⊆ 𝑦 ↔ ∀ 𝑣 ( 𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑦 ) ) |
14 |
|
vpwex |
⊢ 𝒫 𝑧 ∈ V |
15 |
|
sseq1 |
⊢ ( 𝑣 = 𝒫 𝑧 → ( 𝑣 ⊆ 𝑤 ↔ 𝒫 𝑧 ⊆ 𝑤 ) ) |
16 |
|
eleq1 |
⊢ ( 𝑣 = 𝒫 𝑧 → ( 𝑣 ∈ 𝑦 ↔ 𝒫 𝑧 ∈ 𝑦 ) ) |
17 |
15 16
|
imbi12d |
⊢ ( 𝑣 = 𝒫 𝑧 → ( ( 𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑦 ) ↔ ( 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦 ) ) ) |
18 |
14 17
|
spcv |
⊢ ( ∀ 𝑣 ( 𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑦 ) → ( 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦 ) ) |
19 |
13 18
|
sylbi |
⊢ ( 𝒫 𝑤 ⊆ 𝑦 → ( 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦 ) ) |
20 |
12 19
|
syl6 |
⊢ ( ∀ 𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦 → ( 𝑤 ∈ 𝑦 → ( 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦 ) ) ) |
21 |
20
|
rexlimdv |
⊢ ( ∀ 𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦 → ( ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦 ) ) |
22 |
9 21
|
impbid2 |
⊢ ( ∀ 𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦 → ( 𝒫 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) |
23 |
22
|
ralbidv |
⊢ ( ∀ 𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ↔ ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) |
24 |
5 23
|
sylbi |
⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ↔ ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) |
25 |
24
|
pm5.32i |
⊢ ( ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) |
26 |
|
r19.26 |
⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ) |
27 |
|
r19.26 |
⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ↔ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) |
28 |
25 26 27
|
3bitr4i |
⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) |
29 |
|
velpw |
⊢ ( 𝑧 ∈ 𝒫 𝑦 ↔ 𝑧 ⊆ 𝑦 ) |
30 |
|
impexp |
⊢ ( ( ( 𝑧 ⊆ 𝑦 ∧ 𝑧 ≼ 𝑦 ) → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≼ 𝑦 → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) ) |
31 |
|
ssdomg |
⊢ ( 𝑦 ∈ V → ( 𝑧 ⊆ 𝑦 → 𝑧 ≼ 𝑦 ) ) |
32 |
31
|
elv |
⊢ ( 𝑧 ⊆ 𝑦 → 𝑧 ≼ 𝑦 ) |
33 |
32
|
pm4.71i |
⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑧 ⊆ 𝑦 ∧ 𝑧 ≼ 𝑦 ) ) |
34 |
33
|
imbi1i |
⊢ ( ( 𝑧 ⊆ 𝑦 → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ↔ ( ( 𝑧 ⊆ 𝑦 ∧ 𝑧 ≼ 𝑦 ) → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) |
35 |
|
brsdom |
⊢ ( 𝑧 ≺ 𝑦 ↔ ( 𝑧 ≼ 𝑦 ∧ ¬ 𝑧 ≈ 𝑦 ) ) |
36 |
35
|
imbi1i |
⊢ ( ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ( ( 𝑧 ≼ 𝑦 ∧ ¬ 𝑧 ≈ 𝑦 ) → 𝑧 ∈ 𝑦 ) ) |
37 |
|
impexp |
⊢ ( ( ( 𝑧 ≼ 𝑦 ∧ ¬ 𝑧 ≈ 𝑦 ) → 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≼ 𝑦 → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) |
38 |
36 37
|
bitri |
⊢ ( ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≼ 𝑦 → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) |
39 |
38
|
imbi2i |
⊢ ( ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≼ 𝑦 → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) ) |
40 |
30 34 39
|
3bitr4ri |
⊢ ( ( 𝑧 ⊆ 𝑦 → ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑧 ⊆ 𝑦 → ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) |
41 |
40
|
pm5.74ri |
⊢ ( 𝑧 ⊆ 𝑦 → ( ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ) ) |
42 |
|
pm4.64 |
⊢ ( ( ¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) |
43 |
41 42
|
bitrdi |
⊢ ( 𝑧 ⊆ 𝑦 → ( ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) |
44 |
29 43
|
sylbi |
⊢ ( 𝑧 ∈ 𝒫 𝑦 → ( ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) |
45 |
44
|
ralbiia |
⊢ ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) |
46 |
2 28 45
|
3anbi123i |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) |
47 |
46
|
exbii |
⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ) |
48 |
1 47
|
mpbir |
⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) |