Step | Hyp | Ref
| Expression |
1 | | simpll3 1095 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))) → (𝐽 ↾t 𝐴) ∈ Con) |
2 | | simpll1 1093 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | simpll2 1094 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ 𝑋) |
4 | | simplrl 796 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝑥 ∈ 𝐽) |
5 | | simplrr 797 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝑦 ∈ 𝐽) |
6 | | simprl1 1099 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅) |
7 | | n0 3890 |
. . . . . . . . 9
⊢ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) |
8 | 6, 7 | sylib 207 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ∃𝑧 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) |
9 | 2 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ (TopOn‘𝑋)) |
10 | | topontop 20541 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ Top) |
12 | 3 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ 𝑋) |
13 | | toponuni 20542 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
14 | 9, 13 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑋 = ∪ 𝐽) |
15 | 12, 14 | sseqtrd 3604 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ ∪ 𝐽) |
16 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑥 ∩ ((cls‘𝐽)‘𝐴)) ⊆ ((cls‘𝐽)‘𝐴) |
17 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) |
18 | 16, 17 | sseldi 3566 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴)) |
19 | 4 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑥 ∈ 𝐽) |
20 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑥 ∩ ((cls‘𝐽)‘𝐴)) ⊆ 𝑥 |
21 | 20, 17 | sseldi 3566 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ 𝑥) |
22 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
23 | 22 | clsndisj 20689 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽
∧ 𝑧 ∈
((cls‘𝐽)‘𝐴)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑧 ∈ 𝑥)) → (𝑥 ∩ 𝐴) ≠ ∅) |
24 | 11, 15, 18, 19, 21, 23 | syl32anc 1326 |
. . . . . . . 8
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → (𝑥 ∩ 𝐴) ≠ ∅) |
25 | 8, 24 | exlimddv 1850 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝐴) ≠ ∅) |
26 | | simprl2 1100 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅) |
27 | | n0 3890 |
. . . . . . . . 9
⊢ ((𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) |
28 | 26, 27 | sylib 207 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ∃𝑧 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) |
29 | 2 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ (TopOn‘𝑋)) |
30 | 29, 10 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ Top) |
31 | 3 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ 𝑋) |
32 | 29, 13 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑋 = ∪ 𝐽) |
33 | 31, 32 | sseqtrd 3604 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ ∪ 𝐽) |
34 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ⊆ ((cls‘𝐽)‘𝐴) |
35 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) |
36 | 34, 35 | sseldi 3566 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴)) |
37 | 5 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑦 ∈ 𝐽) |
38 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ⊆ 𝑦 |
39 | 38, 35 | sseldi 3566 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ 𝑦) |
40 | 22 | clsndisj 20689 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽
∧ 𝑧 ∈
((cls‘𝐽)‘𝐴)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝑦)) → (𝑦 ∩ 𝐴) ≠ ∅) |
41 | 30, 33, 36, 37, 39, 40 | syl32anc 1326 |
. . . . . . . 8
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → (𝑦 ∩ 𝐴) ≠ ∅) |
42 | 28, 41 | exlimddv 1850 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑦 ∩ 𝐴) ≠ ∅) |
43 | | simprl3 1101 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) |
44 | 2, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐽 ∈ Top) |
45 | 2, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝑋 = ∪ 𝐽) |
46 | 3, 45 | sseqtrd 3604 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ ∪ 𝐽) |
47 | 22 | sscls 20670 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽)
→ 𝐴 ⊆
((cls‘𝐽)‘𝐴)) |
48 | 44, 46, 47 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ ((cls‘𝐽)‘𝐴)) |
49 | 48 | sscond 3709 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑋 ∖ ((cls‘𝐽)‘𝐴)) ⊆ (𝑋 ∖ 𝐴)) |
50 | 43, 49 | sstrd 3578 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ 𝐴)) |
51 | | ssv 3588 |
. . . . . . . . . 10
⊢ 𝑋 ⊆ V |
52 | | ssdif 3707 |
. . . . . . . . . 10
⊢ (𝑋 ⊆ V → (𝑋 ∖ 𝐴) ⊆ (V ∖ 𝐴)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑋 ∖ 𝐴) ⊆ (V ∖ 𝐴) |
54 | 50, 53 | syl6ss 3580 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝑦) ⊆ (V ∖ 𝐴)) |
55 | | disj2 3976 |
. . . . . . . 8
⊢ (((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅ ↔ (𝑥 ∩ 𝑦) ⊆ (V ∖ 𝐴)) |
56 | 54, 55 | sylibr 223 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) |
57 | | simprr 792 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦)) |
58 | 48, 57 | sstrd 3578 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ (𝑥 ∪ 𝑦)) |
59 | 2, 3, 4, 5, 25, 42, 56, 58 | nconsubb 21036 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ¬ (𝐽 ↾t 𝐴) ∈ Con) |
60 | 59 | expr 641 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))) → (((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦) → ¬ (𝐽 ↾t 𝐴) ∈ Con)) |
61 | 1, 60 | mt2d 130 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦)) |
62 | 61 | ex 449 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) |
63 | 62 | ralrimivva 2954 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) |
64 | | simp1 1054 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) → 𝐽 ∈ (TopOn‘𝑋)) |
65 | 13 | sseq2d 3596 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝐽)) |
66 | 65 | biimpa 500 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ 𝐽) |
67 | 22 | clsss3 20673 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝐴) ⊆ ∪ 𝐽) |
68 | 10, 67 | sylan 487 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝐴) ⊆ ∪ 𝐽) |
69 | 66, 68 | syldan 486 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ⊆ ∪ 𝐽) |
70 | 13 | adantr 480 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 = ∪ 𝐽) |
71 | 69, 70 | sseqtr4d 3605 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ⊆ 𝑋) |
72 | 71 | 3adant3 1074 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) → ((cls‘𝐽)‘𝐴) ⊆ 𝑋) |
73 | | connsub 21034 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝐴) ⊆ 𝑋) → ((𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Con ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦)))) |
74 | 64, 72, 73 | syl2anc 691 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) → ((𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Con ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦)))) |
75 | 63, 74 | mpbird 246 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Con) |