Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → 𝑦 ⊆ 𝐽) |
2 | | neibastop1.4 |
. . . . . . . . . 10
⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅} |
3 | | ssrab2 4055 |
. . . . . . . . . 10
⊢ {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋 |
4 | 2, 3 | eqsstri 4000 |
. . . . . . . . 9
⊢ 𝐽 ⊆ 𝒫 𝑋 |
5 | 1, 4 | sstrdi 3978 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → 𝑦 ⊆ 𝒫 𝑋) |
6 | | sspwuni 5014 |
. . . . . . . 8
⊢ (𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦
⊆ 𝑋) |
7 | 5, 6 | sylib 220 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∪ 𝑦 ⊆ 𝑋) |
8 | | vuniex 7459 |
. . . . . . . 8
⊢ ∪ 𝑦
∈ V |
9 | 8 | elpw 4545 |
. . . . . . 7
⊢ (∪ 𝑦
∈ 𝒫 𝑋 ↔
∪ 𝑦 ⊆ 𝑋) |
10 | 7, 9 | sylibr 236 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∪ 𝑦 ∈ 𝒫 𝑋) |
11 | | eluni2 4835 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑦
↔ ∃𝑧 ∈
𝑦 𝑥 ∈ 𝑧) |
12 | | elssuni 4860 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦) |
13 | 12 | ad2antrl 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑦) |
14 | | sspwb 5333 |
. . . . . . . . . . . 12
⊢ (𝑧 ⊆ ∪ 𝑦
↔ 𝒫 𝑧 ⊆
𝒫 ∪ 𝑦) |
15 | 13, 14 | sylib 220 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝒫 𝑧 ⊆ 𝒫 ∪ 𝑦) |
16 | | sslin 4210 |
. . . . . . . . . . 11
⊢
(𝒫 𝑧 ⊆
𝒫 ∪ 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)) |
18 | 1 | sselda 3966 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐽) |
19 | 18 | adantrr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝐽) |
20 | | pweq 4541 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧) |
21 | 20 | ineq2d 4188 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑧)) |
22 | 21 | neeq1d 3075 |
. . . . . . . . . . . . . . 15
⊢ (𝑜 = 𝑧 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
23 | 22 | raleqbi1dv 3403 |
. . . . . . . . . . . . . 14
⊢ (𝑜 = 𝑧 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
24 | 23, 2 | elrab2 3682 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
25 | 24 | simprbi 499 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐽 → ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
26 | 19, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
27 | | simprr 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧) |
28 | | rsp 3205 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥 ∈ 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
29 | 26, 27, 28 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
30 | | ssn0 4353 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅) |
31 | 17, 29, 30 | syl2anc 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅) |
32 | 31 | rexlimdvaa 3285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → (∃𝑧 ∈ 𝑦 𝑥 ∈ 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
33 | 11, 32 | syl5bi 244 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → (𝑥 ∈ ∪ 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
34 | 33 | ralrimiv 3181 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∀𝑥 ∈ ∪ 𝑦((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅) |
35 | | pweq 4541 |
. . . . . . . . . 10
⊢ (𝑜 = ∪
𝑦 → 𝒫 𝑜 = 𝒫 ∪ 𝑦) |
36 | 35 | ineq2d 4188 |
. . . . . . . . 9
⊢ (𝑜 = ∪
𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)) |
37 | 36 | neeq1d 3075 |
. . . . . . . 8
⊢ (𝑜 = ∪
𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
38 | 37 | raleqbi1dv 3403 |
. . . . . . 7
⊢ (𝑜 = ∪
𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ ∪ 𝑦((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
39 | 38, 2 | elrab2 3682 |
. . . . . 6
⊢ (∪ 𝑦
∈ 𝐽 ↔ (∪ 𝑦
∈ 𝒫 𝑋 ∧
∀𝑥 ∈ ∪ 𝑦((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
40 | 10, 34, 39 | sylanbrc 585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∪ 𝑦 ∈ 𝐽) |
41 | 40 | ex 415 |
. . . 4
⊢ (𝜑 → (𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽)) |
42 | 41 | alrimiv 1924 |
. . 3
⊢ (𝜑 → ∀𝑦(𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽)) |
43 | | pweq 4541 |
. . . . . . . . . . 11
⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦) |
44 | 43 | ineq2d 4188 |
. . . . . . . . . 10
⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦)) |
45 | 44 | neeq1d 3075 |
. . . . . . . . 9
⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
46 | 45 | raleqbi1dv 3403 |
. . . . . . . 8
⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
47 | 46, 2 | elrab2 3682 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
48 | 47, 24 | anbi12i 628 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) |
49 | | an4 654 |
. . . . . 6
⊢ (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) |
50 | 48, 49 | bitri 277 |
. . . . 5
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) |
51 | | inss1 4204 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝑧) ⊆ 𝑦 |
52 | | elpwi 4550 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
53 | 51, 52 | sstrid 3977 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝑋 → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
54 | 53 | ad2antrl 726 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
55 | 54 | adantrr 715 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
56 | | vex 3497 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
57 | 56 | inex1 5213 |
. . . . . . . 8
⊢ (𝑦 ∩ 𝑧) ∈ V |
58 | 57 | elpw 4545 |
. . . . . . 7
⊢ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ↔ (𝑦 ∩ 𝑧) ⊆ 𝑋) |
59 | 55, 58 | sylibr 236 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦 ∩ 𝑧) ∈ 𝒫 𝑋) |
60 | | ssralv 4032 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ 𝑧) ⊆ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
61 | 51, 60 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) |
62 | | inss2 4205 |
. . . . . . . . . . 11
⊢ (𝑦 ∩ 𝑧) ⊆ 𝑧 |
63 | | ssralv 4032 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ 𝑧) ⊆ 𝑧 → (∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
65 | 61, 64 | anim12i 614 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
66 | | r19.26 3170 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑦 ∩ 𝑧)(((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
67 | 65, 66 | sylibr 236 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)(((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
68 | | n0 4309 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦)) |
69 | | n0 4309 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) |
70 | 68, 69 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) |
71 | | exdistrv 1952 |
. . . . . . . . . . 11
⊢
(∃𝑣∃𝑤(𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) |
72 | | inss2 4205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦 |
73 | | simprl 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦)) |
74 | 72, 73 | sseldi 3964 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦) |
75 | 74 | elpwid 4552 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ⊆ 𝑦) |
76 | | inss2 4205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧 |
77 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) |
78 | 76, 77 | sseldi 3964 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧) |
79 | 78 | elpwid 4552 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ⊆ 𝑧) |
80 | | ss2in 4212 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ⊆ 𝑦 ∧ 𝑤 ⊆ 𝑧) → (𝑣 ∩ 𝑤) ⊆ (𝑦 ∩ 𝑧)) |
81 | 75, 79, 80 | syl2anc 586 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → (𝑣 ∩ 𝑤) ⊆ (𝑦 ∩ 𝑧)) |
82 | | sspwb 5333 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∩ 𝑤) ⊆ (𝑦 ∩ 𝑧) ↔ 𝒫 (𝑣 ∩ 𝑤) ⊆ 𝒫 (𝑦 ∩ 𝑧)) |
83 | 81, 82 | sylib 220 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣 ∩ 𝑤) ⊆ 𝒫 (𝑦 ∩ 𝑧)) |
84 | | sslin 4210 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 (𝑣 ∩
𝑤) ⊆ 𝒫 (𝑦 ∩ 𝑧) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ⊆ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ⊆ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧))) |
86 | | simplll 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝜑) |
87 | 54 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
88 | | simplr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦 ∩ 𝑧)) |
89 | 87, 88 | sseldd 3967 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ 𝑋) |
90 | | inss1 4204 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹‘𝑥) |
91 | 90, 73 | sseldi 3964 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹‘𝑥)) |
92 | | inss1 4204 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹‘𝑥) |
93 | 92, 77 | sseldi 3964 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹‘𝑥)) |
94 | | neibastop1.3 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) |
95 | 86, 89, 91, 93, 94 | syl13anc 1368 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) |
96 | | ssn0 4353 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ⊆ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ∧ ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
97 | 85, 95, 96 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
98 | 97 | ex 415 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → ((𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
99 | 98 | exlimdvv 1931 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → (∃𝑣∃𝑤(𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
100 | 71, 99 | syl5bir 245 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
101 | 70, 100 | syl5bi 244 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → ((((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
102 | 101 | ralimdva 3177 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦 ∩ 𝑧)(((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
103 | 67, 102 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
104 | 103 | impr 457 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
105 | | pweq 4541 |
. . . . . . . . . 10
⊢ (𝑜 = (𝑦 ∩ 𝑧) → 𝒫 𝑜 = 𝒫 (𝑦 ∩ 𝑧)) |
106 | 105 | ineq2d 4188 |
. . . . . . . . 9
⊢ (𝑜 = (𝑦 ∩ 𝑧) → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧))) |
107 | 106 | neeq1d 3075 |
. . . . . . . 8
⊢ (𝑜 = (𝑦 ∩ 𝑧) → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
108 | 107 | raleqbi1dv 3403 |
. . . . . . 7
⊢ (𝑜 = (𝑦 ∩ 𝑧) → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
109 | 108, 2 | elrab2 3682 |
. . . . . 6
⊢ ((𝑦 ∩ 𝑧) ∈ 𝐽 ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
110 | 59, 104, 109 | sylanbrc 585 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦 ∩ 𝑧) ∈ 𝐽) |
111 | 50, 110 | sylan2b 595 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽)) → (𝑦 ∩ 𝑧) ∈ 𝐽) |
112 | 111 | ralrimivva 3191 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∀𝑧 ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽) |
113 | | neibastop1.1 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
114 | | sspwuni 5014 |
. . . . . . . 8
⊢ (𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽
⊆ 𝑋) |
115 | 4, 114 | mpbi 232 |
. . . . . . 7
⊢ ∪ 𝐽
⊆ 𝑋 |
116 | 115 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ∪ 𝐽
⊆ 𝑋) |
117 | 113, 116 | ssexd 5220 |
. . . . 5
⊢ (𝜑 → ∪ 𝐽
∈ V) |
118 | | uniexb 7480 |
. . . . 5
⊢ (𝐽 ∈ V ↔ ∪ 𝐽
∈ V) |
119 | 117, 118 | sylibr 236 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ V) |
120 | | istopg 21497 |
. . . 4
⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔
(∀𝑦(𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽) ∧ ∀𝑦 ∈ 𝐽 ∀𝑧 ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽))) |
121 | 119, 120 | syl 17 |
. . 3
⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽) ∧ ∀𝑦 ∈ 𝐽 ∀𝑧 ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽))) |
122 | 42, 112, 121 | mpbir2and 711 |
. 2
⊢ (𝜑 → 𝐽 ∈ Top) |
123 | | pwidg 4555 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝒫 𝑋) |
124 | 113, 123 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝒫 𝑋) |
125 | | neibastop1.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖
{∅})) |
126 | 125 | ffvelrnda 6845 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (𝒫 𝒫 𝑋 ∖
{∅})) |
127 | | eldifi 4102 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) →
(𝐹‘𝑥) ∈ 𝒫 𝒫 𝑋) |
128 | | elpwi 4550 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹‘𝑥) ⊆ 𝒫 𝑋) |
129 | 126, 127,
128 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ⊆ 𝒫 𝑋) |
130 | | df-ss 3951 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑋) = (𝐹‘𝑥)) |
131 | 129, 130 | sylib 220 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∩ 𝒫 𝑋) = (𝐹‘𝑥)) |
132 | | eldifsni 4715 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) →
(𝐹‘𝑥) ≠ ∅) |
133 | 126, 132 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≠ ∅) |
134 | 131, 133 | eqnetrd 3083 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅) |
135 | 134 | ralrimiva 3182 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅) |
136 | | pweq 4541 |
. . . . . . . . 9
⊢ (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋) |
137 | 136 | ineq2d 4188 |
. . . . . . . 8
⊢ (𝑜 = 𝑋 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑋)) |
138 | 137 | neeq1d 3075 |
. . . . . . 7
⊢ (𝑜 = 𝑋 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅)) |
139 | 138 | raleqbi1dv 3403 |
. . . . . 6
⊢ (𝑜 = 𝑋 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅)) |
140 | 139, 2 | elrab2 3682 |
. . . . 5
⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅)) |
141 | 124, 135,
140 | sylanbrc 585 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
142 | | elssuni 4860 |
. . . 4
⊢ (𝑋 ∈ 𝐽 → 𝑋 ⊆ ∪ 𝐽) |
143 | 141, 142 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ⊆ ∪ 𝐽) |
144 | 143, 116 | eqssd 3983 |
. 2
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
145 | | istopon 21514 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) |
146 | 122, 144,
145 | sylanbrc 585 |
1
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |