Step | Hyp | Ref
| Expression |
1 | | uniss 4458 |
. . . . . . . 8
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
2 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 |
3 | | sspwuni 4611 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 ↔ ∪ {𝑥
∈ 𝒫 𝐴 ∣
((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ⊆ 𝐴) |
4 | 2, 3 | mpbi 220 |
. . . . . . . 8
⊢ ∪ {𝑥
∈ 𝒫 𝐴 ∣
((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ⊆ 𝐴 |
5 | 1, 4 | syl6ss 3615 |
. . . . . . 7
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
⊆ 𝐴) |
6 | | vuniex 6954 |
. . . . . . . 8
⊢ ∪ 𝑦
∈ V |
7 | 6 | elpw 4164 |
. . . . . . 7
⊢ (∪ 𝑦
∈ 𝒫 𝐴 ↔
∪ 𝑦 ⊆ 𝐴) |
8 | 5, 7 | sylibr 224 |
. . . . . 6
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ 𝒫 𝐴) |
9 | | uni0c 4464 |
. . . . . . . . . . 11
⊢ (∪ 𝑦 =
∅ ↔ ∀𝑧
∈ 𝑦 𝑧 = ∅) |
10 | 9 | notbii 310 |
. . . . . . . . . 10
⊢ (¬
∪ 𝑦 = ∅ ↔ ¬ ∀𝑧 ∈ 𝑦 𝑧 = ∅) |
11 | | rexnal 2995 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑦 ¬ 𝑧 = ∅ ↔ ¬ ∀𝑧 ∈ 𝑦 𝑧 = ∅) |
12 | 10, 11 | bitr4i 267 |
. . . . . . . . 9
⊢ (¬
∪ 𝑦 = ∅ ↔ ∃𝑧 ∈ 𝑦 ¬ 𝑧 = ∅) |
13 | | ssel2 3598 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
14 | | difeq2 3722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑧)) |
15 | 14 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ 𝑧) ≼ ω)) |
16 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝑥 = ∅ ↔ 𝑧 = ∅)) |
17 | 15, 16 | orbi12d 746 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅))) |
18 | 17 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅))) |
19 | 13, 18 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅))) |
20 | 19 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅)) |
21 | 20 | ord 392 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → (¬ (𝐴 ∖ 𝑧) ≼ ω → 𝑧 = ∅)) |
22 | 21 | con1d 139 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 = ∅ → (𝐴 ∖ 𝑧) ≼ ω)) |
23 | 22 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) → (𝐴 ∖ 𝑧) ≼ ω) |
24 | | ctex 7970 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∖ 𝑧) ≼ ω → (𝐴 ∖ 𝑧) ∈ V) |
25 | 24 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) ∧ (𝐴 ∖ 𝑧) ≼ ω) → (𝐴 ∖ 𝑧) ∈ V) |
26 | | simpllr 799 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) ∧ (𝐴 ∖ 𝑧) ≼ ω) → 𝑧 ∈ 𝑦) |
27 | | elssuni 4467 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦) |
28 | | sscon 3744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ ∪ 𝑦
→ (𝐴 ∖ ∪ 𝑦)
⊆ (𝐴 ∖ 𝑧)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) ∧ (𝐴 ∖ 𝑧) ≼ ω) → (𝐴 ∖ ∪ 𝑦) ⊆ (𝐴 ∖ 𝑧)) |
30 | | ssdomg 8001 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∖ 𝑧) ∈ V → ((𝐴 ∖ ∪ 𝑦) ⊆ (𝐴 ∖ 𝑧) → (𝐴 ∖ ∪ 𝑦) ≼ (𝐴 ∖ 𝑧))) |
31 | 25, 29, 30 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) ∧ (𝐴 ∖ 𝑧) ≼ ω) → (𝐴 ∖ ∪ 𝑦) ≼ (𝐴 ∖ 𝑧)) |
32 | | domtr 8009 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∖ ∪ 𝑦)
≼ (𝐴 ∖ 𝑧) ∧ (𝐴 ∖ 𝑧) ≼ ω) → (𝐴 ∖ ∪ 𝑦) ≼
ω) |
33 | 31, 32 | sylancom 701 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) ∧ (𝐴 ∖ 𝑧) ≼ ω) → (𝐴 ∖ ∪ 𝑦) ≼
ω) |
34 | 23, 33 | mpdan 702 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) → (𝐴 ∖ ∪ 𝑦) ≼
ω) |
35 | 34 | exp31 630 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → (𝑧 ∈ 𝑦 → (¬ 𝑧 = ∅ → (𝐴 ∖ ∪ 𝑦) ≼
ω))) |
36 | 35 | rexlimdv 3030 |
. . . . . . . . 9
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → (∃𝑧 ∈ 𝑦 ¬ 𝑧 = ∅ → (𝐴 ∖ ∪ 𝑦) ≼
ω)) |
37 | 12, 36 | syl5bi 232 |
. . . . . . . 8
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → (¬ ∪ 𝑦 =
∅ → (𝐴 ∖
∪ 𝑦) ≼ ω)) |
38 | 37 | con1d 139 |
. . . . . . 7
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → (¬ (𝐴 ∖ ∪ 𝑦) ≼ ω → ∪ 𝑦 =
∅)) |
39 | 38 | orrd 393 |
. . . . . 6
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ((𝐴 ∖ ∪ 𝑦) ≼ ω ∨ ∪ 𝑦 =
∅)) |
40 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = ∪
𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ ∪ 𝑦)) |
41 | 40 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑥 = ∪
𝑦 → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ ∪ 𝑦) ≼
ω)) |
42 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = ∪
𝑦 → (𝑥 = ∅ ↔ ∪ 𝑦 =
∅)) |
43 | 41, 42 | orbi12d 746 |
. . . . . . 7
⊢ (𝑥 = ∪
𝑦 → (((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ ∪ 𝑦) ≼ ω ∨ ∪ 𝑦 =
∅))) |
44 | 43 | elrab 3363 |
. . . . . 6
⊢ (∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ↔ (∪ 𝑦
∈ 𝒫 𝐴 ∧
((𝐴 ∖ ∪ 𝑦)
≼ ω ∨ ∪ 𝑦 = ∅))) |
45 | 8, 39, 44 | sylanbrc 698 |
. . . . 5
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
46 | 45 | ax-gen 1722 |
. . . 4
⊢
∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
47 | | difeq2 3722 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
48 | 47 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ 𝑦) ≼ ω)) |
49 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) |
50 | 48, 49 | orbi12d 746 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ 𝑦) ≼ ω ∨ 𝑦 = ∅))) |
51 | 50 | elrab 3363 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ≼ ω ∨ 𝑦 = ∅))) |
52 | | ssinss1 3841 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝐴 → (𝑦 ∩ 𝑧) ⊆ 𝐴) |
53 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
54 | 53 | elpw 4164 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
55 | 53 | inex1 4799 |
. . . . . . . . . . 11
⊢ (𝑦 ∩ 𝑧) ∈ V |
56 | 55 | elpw 4164 |
. . . . . . . . . 10
⊢ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ↔ (𝑦 ∩ 𝑧) ⊆ 𝐴) |
57 | 52, 54, 56 | 3imtr4i 281 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝐴 → (𝑦 ∩ 𝑧) ∈ 𝒫 𝐴) |
58 | 57 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ≼ ω ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅))) → (𝑦 ∩ 𝑧) ∈ 𝒫 𝐴) |
59 | | difindi 3881 |
. . . . . . . . . . . 12
⊢ (𝐴 ∖ (𝑦 ∩ 𝑧)) = ((𝐴 ∖ 𝑦) ∪ (𝐴 ∖ 𝑧)) |
60 | | unctb 9027 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∖ 𝑦) ≼ ω ∧ (𝐴 ∖ 𝑧) ≼ ω) → ((𝐴 ∖ 𝑦) ∪ (𝐴 ∖ 𝑧)) ≼ ω) |
61 | 59, 60 | syl5eqbr 4688 |
. . . . . . . . . . 11
⊢ (((𝐴 ∖ 𝑦) ≼ ω ∧ (𝐴 ∖ 𝑧) ≼ ω) → (𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω) |
62 | 61 | orcd 407 |
. . . . . . . . . 10
⊢ (((𝐴 ∖ 𝑦) ≼ ω ∧ (𝐴 ∖ 𝑧) ≼ ω) → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅)) |
63 | | ineq1 3807 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (𝑦 ∩ 𝑧) = (∅ ∩ 𝑧)) |
64 | | 0in 3969 |
. . . . . . . . . . . 12
⊢ (∅
∩ 𝑧) =
∅ |
65 | 63, 64 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝑦 ∩ 𝑧) = ∅) |
66 | 65 | olcd 408 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅)) |
67 | | ineq2 3808 |
. . . . . . . . . . . 12
⊢ (𝑧 = ∅ → (𝑦 ∩ 𝑧) = (𝑦 ∩ ∅)) |
68 | | in0 3968 |
. . . . . . . . . . . 12
⊢ (𝑦 ∩ ∅) =
∅ |
69 | 67, 68 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑦 ∩ 𝑧) = ∅) |
70 | 69 | olcd 408 |
. . . . . . . . . 10
⊢ (𝑧 = ∅ → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅)) |
71 | 62, 66, 70 | ccase2 989 |
. . . . . . . . 9
⊢ ((((𝐴 ∖ 𝑦) ≼ ω ∨ 𝑦 = ∅) ∧ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅)) → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅)) |
72 | 71 | ad2ant2l 782 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ≼ ω ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅))) → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅)) |
73 | 58, 72 | jca 554 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ≼ ω ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ≼ ω ∨ 𝑧 = ∅))) → ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅))) |
74 | 51, 18, 73 | syl2anb 496 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) → ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅))) |
75 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑦 ∩ 𝑧))) |
76 | 75 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∩ 𝑧) → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω)) |
77 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝑥 = ∅ ↔ (𝑦 ∩ 𝑧) = ∅)) |
78 | 76, 77 | orbi12d 746 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅))) |
79 | 78 | elrab 3363 |
. . . . . 6
⊢ ((𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ≼ ω ∨ (𝑦 ∩ 𝑧) = ∅))) |
80 | 74, 79 | sylibr 224 |
. . . . 5
⊢ ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) → (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
81 | 80 | rgen2a 2977 |
. . . 4
⊢
∀𝑦 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} |
82 | 46, 81 | pm3.2i 471 |
. . 3
⊢
(∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
83 | | pwexg 4850 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
84 | | rabexg 4812 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → {𝑥 ∈
𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ V) |
85 | | istopg 20700 |
. . . 4
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}))) |
86 | 83, 84, 85 | 3syl 18 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}))) |
87 | 82, 86 | mpbiri 248 |
. 2
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ Top) |
88 | | pwidg 4173 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
89 | | omex 8540 |
. . . . . . . 8
⊢ ω
∈ V |
90 | 89 | 0dom 8090 |
. . . . . . 7
⊢ ∅
≼ ω |
91 | 90 | orci 405 |
. . . . . 6
⊢ (∅
≼ ω ∨ 𝐴 =
∅) |
92 | 91 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∅ ≼ ω ∨ 𝐴 = ∅)) |
93 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝐴)) |
94 | | difid 3948 |
. . . . . . . . 9
⊢ (𝐴 ∖ 𝐴) = ∅ |
95 | 93, 94 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = ∅) |
96 | 95 | breq1d 4663 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝐴 ∖ 𝑥) ≼ ω ↔ ∅ ≼
ω)) |
97 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = ∅ ↔ 𝐴 = ∅)) |
98 | 96, 97 | orbi12d 746 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅) ↔ (∅ ≼ ω
∨ 𝐴 =
∅))) |
99 | 98 | elrab 3363 |
. . . . 5
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ↔ (𝐴 ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ 𝐴 = ∅))) |
100 | 88, 92, 99 | sylanbrc 698 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
101 | | elssuni 4467 |
. . . 4
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} → 𝐴 ⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
102 | 100, 101 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
103 | 4 | a1i 11 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ⊆ 𝐴) |
104 | 102, 103 | eqssd 3620 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 = ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)}) |
105 | | istopon 20717 |
. 2
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ Top ∧ 𝐴 = ∪
{𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)})) |
106 | 87, 104, 105 | sylanbrc 698 |
1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) |