Step | Hyp | Ref
| Expression |
1 | | velpw 4518 |
. . . 4
⊢ (𝑠 ∈ 𝒫 𝐽 ↔ 𝑠 ⊆ 𝐽) |
2 | | simp1l 1199 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝐽 ∈ Comp) |
3 | | simp2 1139 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑠 ⊆ 𝐽) |
4 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | 4 | cldopn 21928 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
6 | 5 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
7 | 6 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) |
8 | 7 | snssd 4722 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → {(∪ 𝐽
∖ 𝑆)} ⊆ 𝐽) |
9 | 3, 8 | unssd 4100 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝐽) |
10 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝑠) |
11 | | uniss 4827 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ⊆ 𝐽 → ∪ 𝑠 ⊆ ∪ 𝐽) |
12 | 11 | 3ad2ant2 1136 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝑠
⊆ ∪ 𝐽) |
13 | 10, 12 | sstrd 3911 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝐽) |
14 | | undif 4396 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ ∪ 𝐽
↔ (𝑆 ∪ (∪ 𝐽
∖ 𝑆)) = ∪ 𝐽) |
15 | 13, 14 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) = ∪ 𝐽) |
16 | | unss1 4093 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ ∪ 𝑠
→ (𝑆 ∪ (∪ 𝐽
∖ 𝑆)) ⊆ (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆))) |
17 | 16 | 3ad2ant3 1137 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ (∪
𝑠 ∪ (∪ 𝐽
∖ 𝑆))) |
18 | 15, 17 | eqsstrrd 3940 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽
⊆ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆))) |
19 | | difss 4046 |
. . . . . . . . . . 11
⊢ (∪ 𝐽
∖ 𝑆) ⊆ ∪ 𝐽 |
20 | | unss 4098 |
. . . . . . . . . . 11
⊢ ((∪ 𝑠
⊆ ∪ 𝐽 ∧ (∪ 𝐽 ∖ 𝑆) ⊆ ∪ 𝐽) ↔ (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪
𝐽) |
21 | 12, 19, 20 | sylanblc 592 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪
𝐽) |
22 | 18, 21 | eqssd 3918 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
(∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆))) |
23 | | uniexg 7528 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Comp → ∪ 𝐽
∈ V) |
24 | 23 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽) → ∪ 𝐽 ∈ V) |
25 | 24 | 3adant3 1134 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽
∈ V) |
26 | | difexg 5220 |
. . . . . . . . . . 11
⊢ (∪ 𝐽
∈ V → (∪ 𝐽 ∖ 𝑆) ∈ V) |
27 | | unisng 4840 |
. . . . . . . . . . 11
⊢ ((∪ 𝐽
∖ 𝑆) ∈ V →
∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆)) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆)) |
29 | 28 | uneq2d 4077 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ (∪ 𝐽
∖ 𝑆))) |
30 | 22, 29 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
(∪ 𝑠 ∪ ∪ {(∪ 𝐽
∖ 𝑆)})) |
31 | | uniun 4844 |
. . . . . . . 8
⊢ ∪ (𝑠
∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) |
32 | 30, 31 | eqtr4di 2796 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) |
33 | 4 | cmpcov 22286 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ⊆ 𝐽 ∧ ∪ 𝐽 =
∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin)∪
𝐽 = ∪ 𝑢) |
34 | 2, 9, 32, 33 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩
Fin)∪ 𝐽 = ∪ 𝑢) |
35 | | elfpw 8978 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩ Fin)
↔ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) |
36 | | simp2l 1201 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) |
37 | | uncom 4067 |
. . . . . . . . . . . 12
⊢ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) = ({(∪ 𝐽
∖ 𝑆)} ∪ 𝑠) |
38 | 36, 37 | sseqtrdi 3951 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑢 ⊆ ({(∪
𝐽 ∖ 𝑆)} ∪ 𝑠)) |
39 | | ssundif 4399 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ ({(∪ 𝐽
∖ 𝑆)} ∪ 𝑠) ↔ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠) |
40 | 38, 39 | sylib 221 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠) |
41 | | diffi 8906 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ Fin → (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
Fin) |
42 | 41 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin) |
43 | 42 | 3adant3 1134 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin) |
44 | | elfpw 8978 |
. . . . . . . . . 10
⊢ ((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
(𝒫 𝑠 ∩ Fin)
↔ ((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ⊆ 𝑠 ∧ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin)) |
45 | 40, 43, 44 | sylanbrc 586 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ (𝒫 𝑠 ∩ Fin)) |
46 | 10 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ 𝑠) |
47 | 12 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝐽) |
48 | | simp3 1140 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝐽 = ∪
𝑢) |
49 | 47, 48 | sseqtrd 3941 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝑢) |
50 | 46, 49 | sstrd 3911 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ 𝑢) |
51 | 50 | sselda 3901 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ ∪ 𝑢) |
52 | | eluni 4822 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ∪ 𝑢
↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢)) |
53 | 51, 52 | sylib 221 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢)) |
54 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤)) |
56 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢)) |
58 | | elndif 4043 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ 𝑆 → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)) |
59 | 58 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)) |
60 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (∪
𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) |
61 | 60 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (∪
𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))) |
63 | 62 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))) |
64 | 63 | imp 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) |
65 | 59, 64 | mtod 201 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆)) |
66 | 65 | ex 416 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))) |
67 | 66 | adantrd 495 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))) |
68 | | velsn 4557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {(∪ 𝐽
∖ 𝑆)} ↔ 𝑤 = (∪
𝐽 ∖ 𝑆)) |
69 | 68 | notbii 323 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ {(∪ 𝐽
∖ 𝑆)} ↔ ¬
𝑤 = (∪ 𝐽
∖ 𝑆)) |
70 | 67, 69 | syl6ibr 255 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})) |
71 | 57, 70 | jcad 516 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)}))) |
72 | | eldif 3876 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})) |
73 | 71, 72 | syl6ibr 255 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) |
74 | 55, 73 | jcad 516 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) |
75 | 74 | eximdv 1925 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) |
76 | 53, 75 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) |
77 | 76 | ex 416 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑣 ∈ 𝑆 → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) |
78 | | eluni 4822 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) |
79 | 77, 78 | syl6ibr 255 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑣 ∈ 𝑆 → 𝑣 ∈ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}))) |
80 | 79 | ssrdv 3907 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)})) |
81 | | unieq 4830 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → ∪
𝑡 = ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)})) |
82 | 81 | sseq2d 3933 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → (𝑆 ⊆ ∪ 𝑡 ↔ 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}))) |
83 | 82 | rspcev 3537 |
. . . . . . . . 9
⊢ (((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
(𝒫 𝑠 ∩ Fin)
∧ 𝑆 ⊆ ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
84 | 45, 80, 83 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
85 | 35, 84 | syl3an2b 1406 |
. . . . . . 7
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ 𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
86 | 85 | rexlimdv3a 3205 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩
Fin)∪ 𝐽 = ∪ 𝑢 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)) |
87 | 34, 86 | mpd 15 |
. . . . 5
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) |
88 | 87 | 3exp 1121 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ⊆ 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
89 | 1, 88 | syl5bi 245 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ∈ 𝒫 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
90 | 89 | ralrimiv 3104 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)) |
91 | | cmptop 22292 |
. . 3
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
92 | 4 | cldss 21926 |
. . 3
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) |
93 | 4 | cmpsub 22297 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((𝐽
↾t 𝑆)
∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
94 | 91, 92, 93 | syl2an 599 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) |
95 | 90, 94 | mpbird 260 |
1
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp) |