Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → 𝑦 ⊆ 𝐽) |
2 | | neibastop1.4 |
. . . . . . . . . 10
⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅} |
3 | | ssrab2 4013 |
. . . . . . . . . 10
⊢ {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋 |
4 | 2, 3 | eqsstri 3955 |
. . . . . . . . 9
⊢ 𝐽 ⊆ 𝒫 𝑋 |
5 | 1, 4 | sstrdi 3933 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → 𝑦 ⊆ 𝒫 𝑋) |
6 | | sspwuni 5029 |
. . . . . . . 8
⊢ (𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦
⊆ 𝑋) |
7 | 5, 6 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∪ 𝑦 ⊆ 𝑋) |
8 | | vuniex 7592 |
. . . . . . . 8
⊢ ∪ 𝑦
∈ V |
9 | 8 | elpw 4537 |
. . . . . . 7
⊢ (∪ 𝑦
∈ 𝒫 𝑋 ↔
∪ 𝑦 ⊆ 𝑋) |
10 | 7, 9 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∪ 𝑦 ∈ 𝒫 𝑋) |
11 | | eluni2 4843 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑦
↔ ∃𝑧 ∈
𝑦 𝑥 ∈ 𝑧) |
12 | | elssuni 4871 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦) |
13 | 12 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑦) |
14 | 13 | sspwd 4548 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝒫 𝑧 ⊆ 𝒫 ∪ 𝑦) |
15 | | sslin 4168 |
. . . . . . . . . . 11
⊢
(𝒫 𝑧 ⊆
𝒫 ∪ 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)) |
17 | 1 | sselda 3921 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐽) |
18 | 17 | adantrr 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝐽) |
19 | | pweq 4549 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧) |
20 | 19 | ineq2d 4146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑧)) |
21 | 20 | neeq1d 3003 |
. . . . . . . . . . . . . . 15
⊢ (𝑜 = 𝑧 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
22 | 21 | raleqbi1dv 3340 |
. . . . . . . . . . . . . 14
⊢ (𝑜 = 𝑧 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
23 | 22, 2 | elrab2 3627 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
24 | 23 | simprbi 497 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐽 → ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
25 | 18, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
26 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧) |
27 | | rsp 3131 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥 ∈ 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
28 | 25, 26, 27 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
29 | | ssn0 4334 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅) |
30 | 16, 28, 29 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅) |
31 | 30 | rexlimdvaa 3214 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → (∃𝑧 ∈ 𝑦 𝑥 ∈ 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
32 | 11, 31 | syl5bi 241 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → (𝑥 ∈ ∪ 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
33 | 32 | ralrimiv 3102 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∀𝑥 ∈ ∪ 𝑦((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅) |
34 | | pweq 4549 |
. . . . . . . . . 10
⊢ (𝑜 = ∪
𝑦 → 𝒫 𝑜 = 𝒫 ∪ 𝑦) |
35 | 34 | ineq2d 4146 |
. . . . . . . . 9
⊢ (𝑜 = ∪
𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)) |
36 | 35 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑜 = ∪
𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
37 | 36 | raleqbi1dv 3340 |
. . . . . . 7
⊢ (𝑜 = ∪
𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ ∪ 𝑦((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
38 | 37, 2 | elrab2 3627 |
. . . . . 6
⊢ (∪ 𝑦
∈ 𝐽 ↔ (∪ 𝑦
∈ 𝒫 𝑋 ∧
∀𝑥 ∈ ∪ 𝑦((𝐹‘𝑥) ∩ 𝒫 ∪ 𝑦)
≠ ∅)) |
39 | 10, 33, 38 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐽) → ∪ 𝑦 ∈ 𝐽) |
40 | 39 | ex 413 |
. . . 4
⊢ (𝜑 → (𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽)) |
41 | 40 | alrimiv 1930 |
. . 3
⊢ (𝜑 → ∀𝑦(𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽)) |
42 | | pweq 4549 |
. . . . . . . . . . 11
⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦) |
43 | 42 | ineq2d 4146 |
. . . . . . . . . 10
⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦)) |
44 | 43 | neeq1d 3003 |
. . . . . . . . 9
⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
45 | 44 | raleqbi1dv 3340 |
. . . . . . . 8
⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
46 | 45, 2 | elrab2 3627 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
47 | 46, 23 | anbi12i 627 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) |
48 | | an4 653 |
. . . . . 6
⊢ (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) |
49 | 47, 48 | bitri 274 |
. . . . 5
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) |
50 | | inss1 4162 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝑧) ⊆ 𝑦 |
51 | | elpwi 4542 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
52 | 50, 51 | sstrid 3932 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝑋 → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
53 | 52 | ad2antrl 725 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
54 | 53 | adantrr 714 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
55 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
56 | 55 | inex1 5241 |
. . . . . . . 8
⊢ (𝑦 ∩ 𝑧) ∈ V |
57 | 56 | elpw 4537 |
. . . . . . 7
⊢ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ↔ (𝑦 ∩ 𝑧) ⊆ 𝑋) |
58 | 54, 57 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦 ∩ 𝑧) ∈ 𝒫 𝑋) |
59 | | ssralv 3987 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ 𝑧) ⊆ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅)) |
60 | 50, 59 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) |
61 | | inss2 4163 |
. . . . . . . . . . 11
⊢ (𝑦 ∩ 𝑧) ⊆ 𝑧 |
62 | | ssralv 3987 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ 𝑧) ⊆ 𝑧 → (∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) |
64 | 60, 63 | anim12i 613 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
65 | | r19.26 3095 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑦 ∩ 𝑧)(((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
66 | 64, 65 | sylibr 233 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)(((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅)) |
67 | | n0 4280 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦)) |
68 | | n0 4280 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) |
69 | 67, 68 | anbi12i 627 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) |
70 | | exdistrv 1959 |
. . . . . . . . . . 11
⊢
(∃𝑣∃𝑤(𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) |
71 | | inss2 4163 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦 |
72 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦)) |
73 | 71, 72 | sselid 3919 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦) |
74 | 73 | elpwid 4544 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ⊆ 𝑦) |
75 | | inss2 4163 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧 |
76 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) |
77 | 75, 76 | sselid 3919 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧) |
78 | 77 | elpwid 4544 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ⊆ 𝑧) |
79 | | ss2in 4170 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ⊆ 𝑦 ∧ 𝑤 ⊆ 𝑧) → (𝑣 ∩ 𝑤) ⊆ (𝑦 ∩ 𝑧)) |
80 | 74, 78, 79 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → (𝑣 ∩ 𝑤) ⊆ (𝑦 ∩ 𝑧)) |
81 | 80 | sspwd 4548 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣 ∩ 𝑤) ⊆ 𝒫 (𝑦 ∩ 𝑧)) |
82 | | sslin 4168 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 (𝑣 ∩
𝑤) ⊆ 𝒫 (𝑦 ∩ 𝑧) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ⊆ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ⊆ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧))) |
84 | | simplll 772 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝜑) |
85 | 53 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → (𝑦 ∩ 𝑧) ⊆ 𝑋) |
86 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦 ∩ 𝑧)) |
87 | 85, 86 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ 𝑋) |
88 | | inss1 4162 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹‘𝑥) |
89 | 88, 72 | sselid 3919 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹‘𝑥)) |
90 | | inss1 4162 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹‘𝑥) |
91 | 90, 76 | sselid 3919 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹‘𝑥)) |
92 | | neibastop1.3 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) |
93 | 84, 87, 89, 91, 92 | syl13anc 1371 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) |
94 | | ssn0 4334 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ⊆ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ∧ ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
95 | 83, 93, 94 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
96 | 95 | ex 413 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → ((𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
97 | 96 | exlimdvv 1937 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → (∃𝑣∃𝑤(𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
98 | 70, 97 | syl5bir 242 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
99 | 69, 98 | syl5bi 241 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦 ∩ 𝑧)) → ((((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
100 | 99 | ralimdva 3108 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦 ∩ 𝑧)(((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
101 | 66, 100 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
102 | 101 | impr 455 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
103 | | pweq 4549 |
. . . . . . . . . 10
⊢ (𝑜 = (𝑦 ∩ 𝑧) → 𝒫 𝑜 = 𝒫 (𝑦 ∩ 𝑧)) |
104 | 103 | ineq2d 4146 |
. . . . . . . . 9
⊢ (𝑜 = (𝑦 ∩ 𝑧) → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧))) |
105 | 104 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑜 = (𝑦 ∩ 𝑧) → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
106 | 105 | raleqbi1dv 3340 |
. . . . . . 7
⊢ (𝑜 = (𝑦 ∩ 𝑧) → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
107 | 106, 2 | elrab2 3627 |
. . . . . 6
⊢ ((𝑦 ∩ 𝑧) ∈ 𝐽 ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦 ∩ 𝑧)((𝐹‘𝑥) ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)) |
108 | 58, 102, 107 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦 ∩ 𝑧) ∈ 𝐽) |
109 | 49, 108 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽)) → (𝑦 ∩ 𝑧) ∈ 𝐽) |
110 | 109 | ralrimivva 3123 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∀𝑧 ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽) |
111 | | neibastop1.1 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
112 | | sspwuni 5029 |
. . . . . . . 8
⊢ (𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽
⊆ 𝑋) |
113 | 4, 112 | mpbi 229 |
. . . . . . 7
⊢ ∪ 𝐽
⊆ 𝑋 |
114 | 113 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ∪ 𝐽
⊆ 𝑋) |
115 | 111, 114 | ssexd 5248 |
. . . . 5
⊢ (𝜑 → ∪ 𝐽
∈ V) |
116 | | uniexb 7614 |
. . . . 5
⊢ (𝐽 ∈ V ↔ ∪ 𝐽
∈ V) |
117 | 115, 116 | sylibr 233 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ V) |
118 | | istopg 22044 |
. . . 4
⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔
(∀𝑦(𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽) ∧ ∀𝑦 ∈ 𝐽 ∀𝑧 ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽))) |
119 | 117, 118 | syl 17 |
. . 3
⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽) ∧ ∀𝑦 ∈ 𝐽 ∀𝑧 ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽))) |
120 | 41, 110, 119 | mpbir2and 710 |
. 2
⊢ (𝜑 → 𝐽 ∈ Top) |
121 | | pwidg 4555 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝒫 𝑋) |
122 | 111, 121 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝒫 𝑋) |
123 | | neibastop1.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖
{∅})) |
124 | 123 | ffvelrnda 6961 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (𝒫 𝒫 𝑋 ∖
{∅})) |
125 | | eldifi 4061 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) →
(𝐹‘𝑥) ∈ 𝒫 𝒫 𝑋) |
126 | | elpwi 4542 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹‘𝑥) ⊆ 𝒫 𝑋) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ⊆ 𝒫 𝑋) |
128 | | df-ss 3904 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑋) = (𝐹‘𝑥)) |
129 | 127, 128 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∩ 𝒫 𝑋) = (𝐹‘𝑥)) |
130 | | eldifsni 4723 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) →
(𝐹‘𝑥) ≠ ∅) |
131 | 124, 130 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≠ ∅) |
132 | 129, 131 | eqnetrd 3011 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅) |
133 | 132 | ralrimiva 3103 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅) |
134 | | pweq 4549 |
. . . . . . . . 9
⊢ (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋) |
135 | 134 | ineq2d 4146 |
. . . . . . . 8
⊢ (𝑜 = 𝑋 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑋)) |
136 | 135 | neeq1d 3003 |
. . . . . . 7
⊢ (𝑜 = 𝑋 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅)) |
137 | 136 | raleqbi1dv 3340 |
. . . . . 6
⊢ (𝑜 = 𝑋 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅)) |
138 | 137, 2 | elrab2 3627 |
. . . . 5
⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑋) ≠ ∅)) |
139 | 122, 133,
138 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
140 | | elssuni 4871 |
. . . 4
⊢ (𝑋 ∈ 𝐽 → 𝑋 ⊆ ∪ 𝐽) |
141 | 139, 140 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ⊆ ∪ 𝐽) |
142 | 141, 114 | eqssd 3938 |
. 2
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
143 | | istopon 22061 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) |
144 | 120, 142,
143 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |