| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | velpw 4604 | . . . 4
⊢ (𝑠 ∈ 𝒫 𝐽 ↔ 𝑠 ⊆ 𝐽) | 
| 2 |  | simp1l 1197 | . . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝐽 ∈ Comp) | 
| 3 |  | simp2 1137 | . . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑠 ⊆ 𝐽) | 
| 4 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 5 | 4 | cldopn 23040 | . . . . . . . . . . 11
⊢ (𝑆 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) | 
| 6 | 5 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) | 
| 7 | 6 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝐽
∖ 𝑆) ∈ 𝐽) | 
| 8 | 7 | snssd 4808 | . . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → {(∪ 𝐽
∖ 𝑆)} ⊆ 𝐽) | 
| 9 | 3, 8 | unssd 4191 | . . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝐽) | 
| 10 |  | simp3 1138 | . . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝑠) | 
| 11 |  | uniss 4914 | . . . . . . . . . . . . . 14
⊢ (𝑠 ⊆ 𝐽 → ∪ 𝑠 ⊆ ∪ 𝐽) | 
| 12 | 11 | 3ad2ant2 1134 | . . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝑠
⊆ ∪ 𝐽) | 
| 13 | 10, 12 | sstrd 3993 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝐽) | 
| 14 |  | undif 4481 | . . . . . . . . . . . 12
⊢ (𝑆 ⊆ ∪ 𝐽
↔ (𝑆 ∪ (∪ 𝐽
∖ 𝑆)) = ∪ 𝐽) | 
| 15 | 13, 14 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) = ∪ 𝐽) | 
| 16 |  | unss1 4184 | . . . . . . . . . . . 12
⊢ (𝑆 ⊆ ∪ 𝑠
→ (𝑆 ∪ (∪ 𝐽
∖ 𝑆)) ⊆ (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆))) | 
| 17 | 16 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ (∪
𝑠 ∪ (∪ 𝐽
∖ 𝑆))) | 
| 18 | 15, 17 | eqsstrrd 4018 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽
⊆ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆))) | 
| 19 |  | difss 4135 | . . . . . . . . . . 11
⊢ (∪ 𝐽
∖ 𝑆) ⊆ ∪ 𝐽 | 
| 20 |  | unss 4189 | . . . . . . . . . . 11
⊢ ((∪ 𝑠
⊆ ∪ 𝐽 ∧ (∪ 𝐽 ∖ 𝑆) ⊆ ∪ 𝐽) ↔ (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪
𝐽) | 
| 21 | 12, 19, 20 | sylanblc 589 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪
𝐽) | 
| 22 | 18, 21 | eqssd 4000 | . . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
(∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆))) | 
| 23 |  | uniexg 7761 | . . . . . . . . . . . . 13
⊢ (𝐽 ∈ Comp → ∪ 𝐽
∈ V) | 
| 24 | 23 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽) → ∪ 𝐽 ∈ V) | 
| 25 | 24 | 3adant3 1132 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽
∈ V) | 
| 26 |  | difexg 5328 | . . . . . . . . . . 11
⊢ (∪ 𝐽
∈ V → (∪ 𝐽 ∖ 𝑆) ∈ V) | 
| 27 |  | unisng 4924 | . . . . . . . . . . 11
⊢ ((∪ 𝐽
∖ 𝑆) ∈ V →
∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆)) | 
| 28 | 25, 26, 27 | 3syl 18 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆)) | 
| 29 | 28 | uneq2d 4167 | . . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠
∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ (∪ 𝐽
∖ 𝑆))) | 
| 30 | 22, 29 | eqtr4d 2779 | . . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
(∪ 𝑠 ∪ ∪ {(∪ 𝐽
∖ 𝑆)})) | 
| 31 |  | uniun 4929 | . . . . . . . 8
⊢ ∪ (𝑠
∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) | 
| 32 | 30, 31 | eqtr4di 2794 | . . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 =
∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) | 
| 33 | 4 | cmpcov 23398 | . . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ⊆ 𝐽 ∧ ∪ 𝐽 =
∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin)∪
𝐽 = ∪ 𝑢) | 
| 34 | 2, 9, 32, 33 | syl3anc 1372 | . . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩
Fin)∪ 𝐽 = ∪ 𝑢) | 
| 35 |  | elfpw 9395 | . . . . . . . 8
⊢ (𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩ Fin)
↔ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) | 
| 36 |  | simp2l 1199 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) | 
| 37 |  | uncom 4157 | . . . . . . . . . . . 12
⊢ (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) = ({(∪ 𝐽
∖ 𝑆)} ∪ 𝑠) | 
| 38 | 36, 37 | sseqtrdi 4023 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑢 ⊆ ({(∪
𝐽 ∖ 𝑆)} ∪ 𝑠)) | 
| 39 |  | ssundif 4487 | . . . . . . . . . . 11
⊢ (𝑢 ⊆ ({(∪ 𝐽
∖ 𝑆)} ∪ 𝑠) ↔ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠) | 
| 40 | 38, 39 | sylib 218 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠) | 
| 41 |  | diffi 9216 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ Fin → (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
Fin) | 
| 42 | 41 | ad2antll 729 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin) | 
| 43 | 42 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin) | 
| 44 |  | elfpw 9395 | . . . . . . . . . 10
⊢ ((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
(𝒫 𝑠 ∩ Fin)
↔ ((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ⊆ 𝑠 ∧ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin)) | 
| 45 | 40, 43, 44 | sylanbrc 583 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ (𝒫 𝑠 ∩ Fin)) | 
| 46 | 10 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ 𝑠) | 
| 47 | 12 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝐽) | 
| 48 |  | simp3 1138 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝐽 = ∪
𝑢) | 
| 49 | 47, 48 | sseqtrd 4019 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝑢) | 
| 50 | 46, 49 | sstrd 3993 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ 𝑢) | 
| 51 | 50 | sselda 3982 | . . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ ∪ 𝑢) | 
| 52 |  | eluni 4909 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ∪ 𝑢
↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢)) | 
| 53 | 51, 52 | sylib 218 | . . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢)) | 
| 54 |  | simpl 482 | . . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤) | 
| 55 | 54 | a1i 11 | . . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤)) | 
| 56 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢) | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢)) | 
| 58 |  | elndif 4132 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ 𝑆 → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)) | 
| 59 | 58 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)) | 
| 60 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (∪
𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) | 
| 61 | 60 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (∪
𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) | 
| 62 | 61 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))) | 
| 63 | 62 | com23 86 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))) | 
| 64 | 63 | imp 406 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))) | 
| 65 | 59, 64 | mtod 198 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆)) | 
| 66 | 65 | ex 412 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))) | 
| 67 | 66 | adantrd 491 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))) | 
| 68 |  | velsn 4641 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {(∪ 𝐽
∖ 𝑆)} ↔ 𝑤 = (∪
𝐽 ∖ 𝑆)) | 
| 69 | 68 | notbii 320 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ {(∪ 𝐽
∖ 𝑆)} ↔ ¬
𝑤 = (∪ 𝐽
∖ 𝑆)) | 
| 70 | 67, 69 | imbitrrdi 252 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})) | 
| 71 | 57, 70 | jcad 512 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)}))) | 
| 72 |  | eldif 3960 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})) | 
| 73 | 71, 72 | imbitrrdi 252 | . . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) | 
| 74 | 55, 73 | jcad 512 | . . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) | 
| 75 | 74 | eximdv 1916 | . . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) | 
| 76 | 53, 75 | mpd 15 | . . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Comp
∧ 𝑆 ∈
(Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) | 
| 77 | 76 | ex 412 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑣 ∈ 𝑆 → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))) | 
| 78 |  | eluni 4909 | . . . . . . . . . . 11
⊢ (𝑣 ∈ ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))) | 
| 79 | 77, 78 | imbitrrdi 252 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → (𝑣 ∈ 𝑆 → 𝑣 ∈ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}))) | 
| 80 | 79 | ssrdv 3988 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)})) | 
| 81 |  | unieq 4917 | . . . . . . . . . . 11
⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → ∪
𝑡 = ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)})) | 
| 82 | 81 | sseq2d 4015 | . . . . . . . . . 10
⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → (𝑆 ⊆ ∪ 𝑡 ↔ 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}))) | 
| 83 | 82 | rspcev 3621 | . . . . . . . . 9
⊢ (((𝑢 ∖ {(∪ 𝐽
∖ 𝑆)}) ∈
(𝒫 𝑠 ∩ Fin)
∧ 𝑆 ⊆ ∪ (𝑢
∖ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) | 
| 84 | 45, 80, 83 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) | 
| 85 | 35, 84 | syl3an2b 1405 | . . . . . . 7
⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ 𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) | 
| 86 | 85 | rexlimdv3a 3158 | . . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽
∖ 𝑆)}) ∩
Fin)∪ 𝐽 = ∪ 𝑢 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)) | 
| 87 | 34, 86 | mpd 15 | . . . . 5
⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡) | 
| 88 | 87 | 3exp 1119 | . . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ⊆ 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) | 
| 89 | 1, 88 | biimtrid 242 | . . 3
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ∈ 𝒫 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) | 
| 90 | 89 | ralrimiv 3144 | . 2
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)) | 
| 91 |  | cmptop 23404 | . . 3
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) | 
| 92 | 4 | cldss 23038 | . . 3
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) | 
| 93 | 4 | cmpsub 23409 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((𝐽
↾t 𝑆)
∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) | 
| 94 | 91, 92, 93 | syl2an 596 | . 2
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))) | 
| 95 | 90, 94 | mpbird 257 | 1
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp) |