Step | Hyp | Ref
| Expression |
1 | | ssrab 3680 |
. . . . 5
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ↔ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) |
2 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → 𝑦 ⊆ 𝒫 𝐴) |
3 | | sspwuni 4611 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝒫 𝐴 ↔ ∪ 𝑦
⊆ 𝐴) |
4 | 2, 3 | sylib 208 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → ∪ 𝑦
⊆ 𝐴) |
5 | | vuniex 6954 |
. . . . . . . . 9
⊢ ∪ 𝑦
∈ V |
6 | 5 | elpw 4164 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ 𝒫 𝐴 ↔
∪ 𝑦 ⊆ 𝐴) |
7 | 4, 6 | sylibr 224 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → ∪ 𝑦
∈ 𝒫 𝐴) |
8 | | neq0 3930 |
. . . . . . . . . 10
⊢ (¬
∪ 𝑦 = ∅ ↔ ∃𝑧 𝑧 ∈ ∪ 𝑦) |
9 | | eluni2 4440 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ 𝑦
↔ ∃𝑥 ∈
𝑦 𝑧 ∈ 𝑥) |
10 | | r19.29 3072 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ ∃𝑥 ∈ 𝑦 𝑧 ∈ 𝑥) → ∃𝑥 ∈ 𝑦 ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥)) |
11 | | n0i 3920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑥 → ¬ 𝑥 = ∅) |
12 | 11 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑥 = ∅) |
13 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥) → (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)) |
14 | 13 | ord 392 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥) → (¬ 𝑃 ∈ 𝑥 → 𝑥 = ∅)) |
15 | 12, 14 | mt3d 140 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥) → 𝑃 ∈ 𝑥) |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑦 ∧ ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥)) → 𝑃 ∈ 𝑥) |
17 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑦 ∧ ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝑦) |
18 | | elunii 4441 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑃 ∈ ∪ 𝑦) |
19 | 16, 17, 18 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑦 ∧ ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥)) → 𝑃 ∈ ∪ 𝑦) |
20 | 19 | rexlimiva 3028 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
𝑦 ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ 𝑧 ∈ 𝑥) → 𝑃 ∈ ∪ 𝑦) |
21 | 10, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ∧ ∃𝑥 ∈ 𝑦 𝑧 ∈ 𝑥) → 𝑃 ∈ ∪ 𝑦) |
22 | 21 | ex 450 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) → (∃𝑥 ∈ 𝑦 𝑧 ∈ 𝑥 → 𝑃 ∈ ∪ 𝑦)) |
23 | 22 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → (∃𝑥 ∈ 𝑦 𝑧 ∈ 𝑥 → 𝑃 ∈ ∪ 𝑦)) |
24 | 9, 23 | syl5bi 232 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → (𝑧 ∈ ∪ 𝑦 → 𝑃 ∈ ∪ 𝑦)) |
25 | 24 | exlimdv 1861 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → (∃𝑧 𝑧 ∈ ∪ 𝑦 → 𝑃 ∈ ∪ 𝑦)) |
26 | 8, 25 | syl5bi 232 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → (¬ ∪ 𝑦 =
∅ → 𝑃 ∈
∪ 𝑦)) |
27 | 26 | con1d 139 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → (¬ 𝑃 ∈ ∪ 𝑦 → ∪ 𝑦 =
∅)) |
28 | 27 | orrd 393 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → (𝑃 ∈ ∪ 𝑦 ∨ ∪ 𝑦 =
∅)) |
29 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑥 = ∪
𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ∪ 𝑦)) |
30 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑥 = ∪
𝑦 → (𝑥 = ∅ ↔ ∪ 𝑦 =
∅)) |
31 | 29, 30 | orbi12d 746 |
. . . . . . . 8
⊢ (𝑥 = ∪
𝑦 → ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ↔ (𝑃 ∈ ∪ 𝑦 ∨ ∪ 𝑦 =
∅))) |
32 | 31 | elrab 3363 |
. . . . . . 7
⊢ (∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ↔ (∪ 𝑦
∈ 𝒫 𝐴 ∧
(𝑃 ∈ ∪ 𝑦
∨ ∪ 𝑦 = ∅))) |
33 | 7, 28, 32 | sylanbrc 698 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅))) → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
34 | 33 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ((𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥 ∈ 𝑦 (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)) → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)})) |
35 | 1, 34 | syl5bi 232 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)})) |
36 | 35 | alrimiv 1855 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)})) |
37 | | eleq2 2690 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦)) |
38 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) |
39 | 37, 38 | orbi12d 746 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ↔ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅))) |
40 | 39 | elrab 3363 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅))) |
41 | | eleq2 2690 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑧)) |
42 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 = ∅ ↔ 𝑧 = ∅)) |
43 | 41, 42 | orbi12d 746 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ↔ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅))) |
44 | 43 | elrab 3363 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅))) |
45 | 40, 44 | anbi12i 733 |
. . . . 5
⊢ ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) |
46 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝑦 ∩ 𝑧) ⊆ 𝑦 |
47 | | simprll 802 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → 𝑦 ∈ 𝒫 𝐴) |
48 | 47 | elpwid 4170 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → 𝑦 ⊆ 𝐴) |
49 | 46, 48 | syl5ss 3614 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (𝑦 ∩ 𝑧) ⊆ 𝐴) |
50 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
51 | 50 | inex1 4799 |
. . . . . . . . 9
⊢ (𝑦 ∩ 𝑧) ∈ V |
52 | 51 | elpw 4164 |
. . . . . . . 8
⊢ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ↔ (𝑦 ∩ 𝑧) ⊆ 𝐴) |
53 | 49, 52 | sylibr 224 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (𝑦 ∩ 𝑧) ∈ 𝒫 𝐴) |
54 | | ianor 509 |
. . . . . . . . . . 11
⊢ (¬
(𝑃 ∈ 𝑦 ∧ 𝑃 ∈ 𝑧) ↔ (¬ 𝑃 ∈ 𝑦 ∨ ¬ 𝑃 ∈ 𝑧)) |
55 | | elin 3796 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (𝑦 ∩ 𝑧) ↔ (𝑃 ∈ 𝑦 ∧ 𝑃 ∈ 𝑧)) |
56 | 54, 55 | xchnxbir 323 |
. . . . . . . . . 10
⊢ (¬
𝑃 ∈ (𝑦 ∩ 𝑧) ↔ (¬ 𝑃 ∈ 𝑦 ∨ ¬ 𝑃 ∈ 𝑧)) |
57 | | simprlr 803 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) |
58 | 57 | ord 392 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (¬ 𝑃 ∈ 𝑦 → 𝑦 = ∅)) |
59 | | simprrr 805 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)) |
60 | 59 | ord 392 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (¬ 𝑃 ∈ 𝑧 → 𝑧 = ∅)) |
61 | 58, 60 | orim12d 883 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → ((¬ 𝑃 ∈ 𝑦 ∨ ¬ 𝑃 ∈ 𝑧) → (𝑦 = ∅ ∨ 𝑧 = ∅))) |
62 | 56, 61 | syl5bi 232 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (¬ 𝑃 ∈ (𝑦 ∩ 𝑧) → (𝑦 = ∅ ∨ 𝑧 = ∅))) |
63 | | inss 3842 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅) → (𝑦 ∩ 𝑧) ⊆ ∅) |
64 | | ss0b 3973 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ∅ ↔ 𝑦 = ∅) |
65 | | ss0b 3973 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ ∅ ↔ 𝑧 = ∅) |
66 | 64, 65 | orbi12i 543 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅) ↔ (𝑦 = ∅ ∨ 𝑧 = ∅)) |
67 | | ss0b 3973 |
. . . . . . . . . 10
⊢ ((𝑦 ∩ 𝑧) ⊆ ∅ ↔ (𝑦 ∩ 𝑧) = ∅) |
68 | 63, 66, 67 | 3imtr3i 280 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∨ 𝑧 = ∅) → (𝑦 ∩ 𝑧) = ∅) |
69 | 62, 68 | syl6 35 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (¬ 𝑃 ∈ (𝑦 ∩ 𝑧) → (𝑦 ∩ 𝑧) = ∅)) |
70 | 69 | orrd 393 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (𝑃 ∈ (𝑦 ∩ 𝑧) ∨ (𝑦 ∩ 𝑧) = ∅)) |
71 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ (𝑦 ∩ 𝑧))) |
72 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝑥 = ∅ ↔ (𝑦 ∩ 𝑧) = ∅)) |
73 | 71, 72 | orbi12d 746 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∩ 𝑧) → ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ↔ (𝑃 ∈ (𝑦 ∩ 𝑧) ∨ (𝑦 ∩ 𝑧) = ∅))) |
74 | 73 | elrab 3363 |
. . . . . . 7
⊢ ((𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦 ∩ 𝑧) ∨ (𝑦 ∩ 𝑧) = ∅))) |
75 | 53, 70, 74 | sylanbrc 698 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅)))) → (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
76 | 75 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → (((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 ∨ 𝑧 = ∅))) → (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)})) |
77 | 45, 76 | syl5bi 232 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) → (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)})) |
78 | 77 | ralrimivv 2970 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
79 | | pwexg 4850 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
80 | 79 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → 𝒫 𝐴 ∈ V) |
81 | | rabexg 4812 |
. . . . 5
⊢
(𝒫 𝐴 ∈
V → {𝑥 ∈
𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ V) |
82 | 80, 81 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ V) |
83 | | istopg 20700 |
. . . 4
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}))) |
84 | 82, 83 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}))) |
85 | 36, 78, 84 | mpbir2and 957 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ Top) |
86 | | pwidg 4173 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
87 | 86 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → 𝐴 ∈ 𝒫 𝐴) |
88 | | simpr 477 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐴) |
89 | 88 | orcd 407 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → (𝑃 ∈ 𝐴 ∨ 𝐴 = ∅)) |
90 | | eleq2 2690 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝐴)) |
91 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = ∅ ↔ 𝐴 = ∅)) |
92 | 90, 91 | orbi12d 746 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑃 ∈ 𝑥 ∨ 𝑥 = ∅) ↔ (𝑃 ∈ 𝐴 ∨ 𝐴 = ∅))) |
93 | 92 | elrab 3363 |
. . . . 5
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ↔ (𝐴 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝐴 ∨ 𝐴 = ∅))) |
94 | 87, 89, 93 | sylanbrc 698 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
95 | | elssuni 4467 |
. . . 4
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} → 𝐴 ⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
96 | 94, 95 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → 𝐴 ⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
97 | | ssrab2 3687 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 |
98 | | sspwuni 4611 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 ↔ ∪ {𝑥
∈ 𝒫 𝐴 ∣
(𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ⊆ 𝐴) |
99 | 97, 98 | mpbi 220 |
. . . 4
⊢ ∪ {𝑥
∈ 𝒫 𝐴 ∣
(𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ⊆ 𝐴 |
100 | 99 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ∪ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ⊆ 𝐴) |
101 | 96, 100 | eqssd 3620 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → 𝐴 = ∪ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)}) |
102 | | istopon 20717 |
. 2
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ Top ∧ 𝐴 = ∪
{𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)})) |
103 | 85, 101, 102 | sylanbrc 698 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) |