Step | Hyp | Ref
| Expression |
1 | | selpw 4115 |
. . . 4
⊢ (𝑠 ∈ 𝒫 𝐽 ↔ 𝑠 ⊆ 𝐽) |
2 | | simp1l 1078 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝐽 ∈ Comp) |
3 | | simp2 1055 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑠 ⊆ 𝐽) |
4 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | 4 | cldopn 20645 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
6 | 5 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
7 | 6 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
8 | 7 | snssd 4281 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → {(∪ 𝐽
∖ 𝑆)} ⊆ 𝐽) |
9 | 3, 8 | unssd 3751 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝐽) |
10 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝑠) |
11 | | uniss 4394 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ⊆ 𝐽 → ∪ 𝑠 ⊆ ∪ 𝐽) |
12 | 11 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝑠
⊆ ∪ 𝐽) |
13 | 10, 12 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝐽) |
14 | | undif 4001 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ ∪ 𝐽
↔ (𝑆 ∪ (∪ 𝐽
∖ 𝑆)) = ∪ 𝐽) |
15 | 13, 14 | sylib 207 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) = ∪ 𝐽) |
16 | | unss1 3744 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ ∪ 𝑠
→ (𝑆 ∪ (∪ 𝐽
∖ 𝑆)) ⊆ (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆))) |
17 | 16 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ (∪
𝑠 ∪ (∪ 𝐽
∖ 𝑆))) |
18 | 15, 17 | eqsstr3d 3603 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽
⊆ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆))) |
19 | | difss 3699 |
. . . . . . . . . . . 12
⊢ (∪ 𝐽
∖ 𝑆) ⊆ ∪ 𝐽 |
20 | 12, 19 | jctir 559 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
⊆ ∪ 𝐽 ∧ (∪ 𝐽 ∖ 𝑆) ⊆ ∪ 𝐽)) |
21 | | unss 3749 |
. . . . . . . . . . 11
⊢ ((∪ 𝑠
⊆ ∪ 𝐽 ∧ (∪ 𝐽 ∖ 𝑆) ⊆ ∪ 𝐽) ↔ (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪
𝐽) |
22 | 20, 21 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪
𝐽) |
23 | 18, 22 | eqssd 3585 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
(∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆))) |
24 | | uniexg 6853 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Comp → ∪ 𝐽
∈ V) |
25 | 24 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽) → ∪ 𝐽 ∈ V) |
26 | 25 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽
∈ V) |
27 | | difexg 4735 |
. . . . . . . . . . 11
⊢ (∪ 𝐽
∈ V → (∪ 𝐽 ∖ 𝑆) ∈ V) |
28 | | unisng 4388 |
. . . . . . . . . . 11
⊢ ((∪ 𝐽
∖ 𝑆) ∈ V →
∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆)) |
30 | 29 | uneq2d 3729 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ (∪ 𝐽
∖ 𝑆))) |
31 | 23, 30 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
(∪ 𝑠 ∪ ∪ {(∪ 𝐽
∖ 𝑆)})) |
32 | | uniun 4392 |
. . . . . . . 8
⊢ ∪ (𝑠
∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) |
33 | 31, 32 | syl6eqr 2662 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) |
34 | 4 | cmpcov 21002 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ⊆ 𝐽 ∧ ∪ 𝐽 =
∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin)∪
𝐽 = ∪ 𝑢) |
35 | 2, 9, 33, 34 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩
Fin)∪ 𝐽 = ∪ 𝑢) |
36 | | elfpw 8151 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩ Fin)
↔ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) |
37 | | simp2l 1080 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) |
38 | | uncom 3719 |
. . . . . . . . . . . 12
⊢ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) = ({(∪ 𝐽
∖ 𝑆)} ∪ 𝑠) |
39 | 37, 38 | syl6sseq 3614 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑢 ⊆ ({(∪
𝐽 ∖ 𝑆)} ∪ 𝑠)) |
40 | | ssundif 4004 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ ({(∪ 𝐽
∖ 𝑆)} ∪ 𝑠) ↔ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠) |
41 | 39, 40 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠) |
42 | | diffi 8077 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ Fin → (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
Fin) |
43 | 42 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin) |
44 | 43 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin) |
45 | | elfpw 8151 |
. . . . . . . . . 10
⊢ ((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
(𝒫 𝑠 ∩ Fin)
↔ ((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ⊆ 𝑠 ∧ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin)) |
46 | 41, 44, 45 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ (𝒫 𝑠 ∩ Fin)) |
47 | 10 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ 𝑠) |
48 | 12 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝐽) |
49 | | simp3 1056 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝐽 = ∪
𝑢) |
50 | 48, 49 | sseqtrd 3604 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝑢) |
51 | 47, 50 | sstrd 3578 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ 𝑢) |
52 | 51 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ ∪ 𝑢) |
53 | | eluni 4375 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ∪ 𝑢
↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢)) |
54 | 52, 53 | sylib 207 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢)) |
55 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤) |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤)) |
57 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢)) |
59 | | elndif 3696 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ 𝑆 → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)) |
60 | 59 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)) |
61 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (∪
𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) |
62 | 61 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (∪
𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))) |
64 | 63 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))) |
65 | 64 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) |
66 | 60, 65 | mtod 188 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆)) |
67 | 66 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))) |
68 | 67 | adantrd 483 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))) |
69 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {(∪ 𝐽
∖ 𝑆)} ↔ 𝑤 = (∪
𝐽 ∖ 𝑆)) |
70 | 69 | notbii 309 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ {(∪ 𝐽
∖ 𝑆)} ↔ ¬
𝑤 = (∪ 𝐽
∖ 𝑆)) |
71 | 68, 70 | syl6ibr 241 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})) |
72 | 58, 71 | jcad 554 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)}))) |
73 | | eldif 3550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})) |
74 | 72, 73 | syl6ibr 241 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) |
75 | 56, 74 | jcad 554 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) |
76 | 75 | eximdv 1833 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) |
77 | 54, 76 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) |
78 | 77 | ex 449 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑣 ∈ 𝑆 → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) |
79 | | eluni 4375 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) |
80 | 78, 79 | syl6ibr 241 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑣 ∈ 𝑆 → 𝑣 ∈ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}))) |
81 | 80 | ssrdv 3574 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)})) |
82 | | unieq 4380 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → ∪
𝑡 = ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)})) |
83 | 82 | sseq2d 3596 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → (𝑆 ⊆ ∪ 𝑡 ↔ 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}))) |
84 | 83 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
(𝒫 𝑠 ∩ Fin)
∧ 𝑆 ⊆ ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
85 | 46, 81, 84 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
86 | 36, 85 | syl3an2b 1355 |
. . . . . . 7
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ 𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
87 | 86 | rexlimdv3a 3015 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩
Fin)∪ 𝐽 = ∪ 𝑢 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)) |
88 | 35, 87 | mpd 15 |
. . . . 5
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
89 | 88 | 3exp 1256 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ⊆ 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
90 | 1, 89 | syl5bi 231 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ∈ 𝒫 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
91 | 90 | ralrimiv 2948 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)) |
92 | | cmptop 21008 |
. . 3
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
93 | 4 | cldss 20643 |
. . 3
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) |
94 | 4 | cmpsub 21013 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((𝐽
↾t 𝑆)
∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
95 | 92, 93, 94 | syl2an 493 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
96 | 91, 95 | mpbird 246 |
1
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp) |