| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) | 
| 2 | 1 | iscmp 23396 | . . 3
⊢ ((𝐽 ↾t 𝑆) ∈ Comp ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | 
| 3 |  | id 22 | . . . . . 6
⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋) | 
| 4 |  | cmpsub.1 | . . . . . . 7
⊢ 𝑋 = ∪
𝐽 | 
| 5 | 4 | topopn 22912 | . . . . . 6
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) | 
| 6 |  | ssexg 5323 | . . . . . 6
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V) | 
| 7 | 3, 5, 6 | syl2anr 597 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) | 
| 8 |  | resttop 23168 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top) | 
| 9 | 7, 8 | syldan 591 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top) | 
| 10 |  | ibar 528 | . . . . 5
⊢ ((𝐽 ↾t 𝑆) ∈ Top →
(∀𝑠 ∈ 𝒫
(𝐽 ↾t
𝑆)(∪ (𝐽
↾t 𝑆) =
∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
↔ ((𝐽
↾t 𝑆)
∈ Top ∧ ∀𝑠
∈ 𝒫 (𝐽
↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)))) | 
| 11 | 10 | bicomd 223 | . . . 4
⊢ ((𝐽 ↾t 𝑆) ∈ Top → (((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | 
| 12 | 9, 11 | syl 17 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | 
| 13 | 2, 12 | bitrid 283 | . 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | 
| 14 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑡 ∈ V | 
| 15 |  | eqeq1 2741 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑡 = (𝑦 ∩ 𝑆))) | 
| 16 | 15 | rexbidv 3179 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆))) | 
| 17 | 14, 16 | elab 3679 | . . . . . . . . . 10
⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆)) | 
| 18 |  | velpw 4605 | . . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽) | 
| 19 |  | ssel2 3978 | . . . . . . . . . . . . . . . 16
⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → 𝑦 ∈ 𝐽) | 
| 20 |  | ineq1 4213 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑦 → (𝑑 ∩ 𝑆) = (𝑦 ∩ 𝑆)) | 
| 21 | 20 | rspceeqv 3645 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑡 = (𝑦 ∩ 𝑆)) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)) | 
| 22 | 21 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐽 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) | 
| 23 | 19, 22 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) | 
| 24 | 23 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝑐 ⊆ 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))) | 
| 25 | 18, 24 | sylbi 217 | . . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝒫 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))) | 
| 26 | 25 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))) | 
| 27 | 26 | rexlimdv 3153 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) | 
| 28 |  | simpll 767 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top) | 
| 29 | 4 | sseq2i 4013 | . . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽) | 
| 30 |  | uniexg 7760 | . . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) | 
| 31 |  | ssexg 5323 | . . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ ∪ 𝐽
∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V) | 
| 32 | 30, 31 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ∪ 𝐽
∧ 𝐽 ∈ Top) →
𝑆 ∈
V) | 
| 33 | 32 | ancoms 458 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ 𝑆 ∈
V) | 
| 34 | 29, 33 | sylan2b 594 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) | 
| 35 | 34 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V) | 
| 36 |  | elrest 17472 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) | 
| 37 | 28, 35, 36 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) | 
| 38 | 27, 37 | sylibrd 259 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → 𝑡 ∈ (𝐽 ↾t 𝑆))) | 
| 39 | 17, 38 | biimtrid 242 | . . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝑡 ∈ (𝐽 ↾t 𝑆))) | 
| 40 | 39 | ssrdv 3989 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆)) | 
| 41 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑐 ∈ V | 
| 42 | 41 | abrexex 7987 | . . . . . . . . 9
⊢ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ V | 
| 43 | 42 | elpw 4604 | . . . . . . . 8
⊢ ({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ↔ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆)) | 
| 44 | 40, 43 | sylibr 234 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆)) | 
| 45 |  | unieq 4918 | . . . . . . . . . 10
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∪ 𝑠 = ∪
{𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) | 
| 46 | 45 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})) | 
| 47 |  | pweq 4614 | . . . . . . . . . . 11
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) | 
| 48 | 47 | ineq1d 4219 | . . . . . . . . . 10
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) | 
| 49 | 48 | rexeqdv 3327 | . . . . . . . . 9
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡
↔ ∃𝑡 ∈
(𝒫 {𝑥 ∣
∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) | 
| 50 | 46, 49 | imbi12d 344 | . . . . . . . 8
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ((∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ (∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) | 
| 51 | 50 | rspcva 3620 | . . . . . . 7
⊢ (({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) → (∪
(𝐽 ↾t
𝑆) = ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) | 
| 52 | 44, 51 | sylan 580 | . . . . . 6
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) → (∪
(𝐽 ↾t
𝑆) = ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) | 
| 53 | 52 | ex 412 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) → (∪ (𝐽 ↾t 𝑆) = ∪
{𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) | 
| 54 | 4 | restuni 23170 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) | 
| 55 | 54 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) | 
| 56 |  | vex 3484 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V | 
| 57 | 56 | inex1 5317 | . . . . . . . . . . . . 13
⊢ (𝑦 ∩ 𝑆) ∈ V | 
| 58 | 57 | dfiun2 5033 | . . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} | 
| 59 |  | incom 4209 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦) | 
| 60 | 59 | a1i 11 | . . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑦 ∈ 𝑐) → (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦)) | 
| 61 | 60 | iuneq2dv 5016 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪
𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦)) | 
| 62 | 58, 61 | eqtr3id 2791 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} = ∪
𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦)) | 
| 63 |  | iunin2 5071 | . . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = (𝑆 ∩ ∪
𝑦 ∈ 𝑐 𝑦) | 
| 64 |  | uniiun 5058 | . . . . . . . . . . . . . . . 16
⊢ ∪ 𝑐 =
∪ 𝑦 ∈ 𝑐 𝑦 | 
| 65 | 64 | eqcomi 2746 | . . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐 | 
| 66 | 65 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐) | 
| 67 | 66 | ineq2d 4220 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪
𝑦 ∈ 𝑐 𝑦) = (𝑆 ∩ ∪ 𝑐)) | 
| 68 |  | incom 4209 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ∩ ∪ 𝑐) =
(∪ 𝑐 ∩ 𝑆) | 
| 69 |  | sseqin2 4223 | . . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ ∪ 𝑐
↔ (∪ 𝑐 ∩ 𝑆) = 𝑆) | 
| 70 | 69 | biimpi 216 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ⊆ ∪ 𝑐
→ (∪ 𝑐 ∩ 𝑆) = 𝑆) | 
| 71 | 68, 70 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ ∪ 𝑐
→ (𝑆 ∩ ∪ 𝑐) =
𝑆) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑐) = 𝑆) | 
| 73 | 67, 72 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪
𝑦 ∈ 𝑐 𝑦) = 𝑆) | 
| 74 | 63, 73 | eqtrid 2789 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = 𝑆) | 
| 75 | 62, 74 | eqtr2d 2778 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) | 
| 76 | 55, 75 | eqeq12d 2753 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = 𝑆 ↔ ∪ (𝐽 ↾t 𝑆) = ∪
{𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})) | 
| 77 | 55 | eqeq1d 2739 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = ∪ 𝑡 ↔ ∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) | 
| 78 | 77 | rexbidv 3179 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) | 
| 79 | 76, 78 | imbi12d 344 | . . . . . . . 8
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) ↔ (∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) | 
| 80 |  | eqid 2737 | . . . . . . . . . 10
⊢ 𝑆 = 𝑆 | 
| 81 | 80 | a1bi 362 | . . . . . . . . 9
⊢
(∃𝑡 ∈
(𝒫 {𝑥 ∣
∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡)) | 
| 82 |  | elin 3967 | . . . . . . . . . . . 12
⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin)) | 
| 83 |  | velpw 4605 | . . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) | 
| 84 |  | dfss3 3972 | . . . . . . . . . . . . . 14
⊢ (𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) | 
| 85 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V | 
| 86 |  | eqeq1 2741 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑠 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑠 = (𝑦 ∩ 𝑆))) | 
| 87 | 86 | rexbidv 3179 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))) | 
| 88 | 85, 87 | elab 3679 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) | 
| 89 | 88 | ralbii 3093 | . . . . . . . . . . . . . 14
⊢
(∀𝑠 ∈
𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) | 
| 90 | 83, 84, 89 | 3bitri 297 | . . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) | 
| 91 | 90 | anbi1i 624 | . . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) | 
| 92 | 82, 91 | bitri 275 | . . . . . . . . . . 11
⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) | 
| 93 |  | ineq1 4213 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑓‘𝑠) → (𝑦 ∩ 𝑆) = ((𝑓‘𝑠) ∩ 𝑆)) | 
| 94 | 93 | eqeq2d 2748 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑓‘𝑠) → (𝑠 = (𝑦 ∩ 𝑆) ↔ 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) | 
| 95 | 94 | ac6sfi 9320 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) | 
| 96 | 95 | ancoms 458 | . . . . . . . . . . . . 13
⊢
((∀𝑠 ∈
𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) | 
| 97 | 96 | adantl 481 | . . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) | 
| 98 |  | frn 6743 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑡⟶𝑐 → ran 𝑓 ⊆ 𝑐) | 
| 99 | 98 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ⊆ 𝑐) | 
| 100 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑓 ∈ V | 
| 101 | 100 | rnex 7932 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ran 𝑓 ∈ V | 
| 102 | 101 | elpw 4604 | . . . . . . . . . . . . . . . . . . . 20
⊢ (ran
𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐) | 
| 103 | 99, 102 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐) | 
| 104 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin) | 
| 105 | 104 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin) | 
| 106 |  | ffn 6736 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑡⟶𝑐 → 𝑓 Fn 𝑡) | 
| 107 |  | dffn4 6826 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑡 ↔ 𝑓:𝑡–onto→ran 𝑓) | 
| 108 | 106, 107 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:𝑡⟶𝑐 → 𝑓:𝑡–onto→ran 𝑓) | 
| 109 |  | fodomfi 9350 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡–onto→ran 𝑓) → ran 𝑓 ≼ 𝑡) | 
| 110 | 108, 109 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡) | 
| 111 | 110 | adantll 714 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((∀𝑠 ∈
𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡) | 
| 112 | 111 | adantll 714 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡) | 
| 113 | 112 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ≼ 𝑡) | 
| 114 |  | domfi 9229 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡) → ran 𝑓 ∈ Fin) | 
| 115 | 105, 113,
114 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin) | 
| 116 | 103, 115 | elind 4200 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin)) | 
| 117 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 = 𝑢 → 𝑠 = 𝑢) | 
| 118 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑢 → (𝑓‘𝑠) = (𝑓‘𝑢)) | 
| 119 | 118 | ineq1d 4219 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 = 𝑢 → ((𝑓‘𝑠) ∩ 𝑆) = ((𝑓‘𝑢) ∩ 𝑆)) | 
| 120 | 117, 119 | eqeq12d 2753 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑠 = 𝑢 → (𝑠 = ((𝑓‘𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) | 
| 121 | 120 | rspccv 3619 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑠 ∈
𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆) → (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) | 
| 122 |  | pm2.27 42 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) | 
| 123 |  | inss1 4237 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢) | 
| 124 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓‘𝑢) ↔ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢))) | 
| 125 | 123, 124 | mpbiri 258 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓‘𝑢)) | 
| 126 |  | ssel 3977 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (𝑓‘𝑢))) | 
| 127 | 126 | a1dd 50 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))) | 
| 128 | 125, 127 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))) | 
| 129 | 128 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))) | 
| 130 | 129 | 3imp 1111 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))) | 
| 131 |  | fnfvelrn 7100 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → (𝑓‘𝑢) ∈ ran 𝑓) | 
| 132 | 131 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 ∈ 𝑡 → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓)) | 
| 133 | 132 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓)) | 
| 134 | 106, 133 | syl5 34 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑓‘𝑢) ∈ ran 𝑓)) | 
| 135 | 130, 134 | jcad 512 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) | 
| 136 | 135 | 3exp 1120 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))) | 
| 137 | 122, 136 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))) | 
| 138 | 137 | com3r 87 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ 𝑢 → (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))) | 
| 139 | 138 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))) | 
| 140 | 139 | com3l 89 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))) | 
| 141 | 140 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:𝑡⟶𝑐 ∧ (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) | 
| 142 | 121, 141 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) | 
| 143 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓‘𝑢) ∈ V | 
| 144 |  | eleq2 2830 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = (𝑓‘𝑢) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ (𝑓‘𝑢))) | 
| 145 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = (𝑓‘𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓‘𝑢) ∈ ran 𝑓)) | 
| 146 | 144, 145 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = (𝑓‘𝑢) → ((𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) | 
| 147 | 143, 146 | spcev 3606 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)) | 
| 148 | 142, 147 | syl6 35 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))) | 
| 149 | 148 | exlimdv 1933 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))) | 
| 150 |  | eluni 4910 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ∪ 𝑡
↔ ∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡)) | 
| 151 |  | eluni 4910 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ∪ ran 𝑓 ↔ ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)) | 
| 152 | 149, 150,
151 | 3imtr4g 296 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran
𝑓)) | 
| 153 | 152 | ssrdv 3989 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∪ 𝑡 ⊆ ∪ ran 𝑓) | 
| 154 | 153 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ∪
𝑡 ⊆ ∪ ran 𝑓) | 
| 155 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 = ∪
𝑡 → (𝑆 ⊆ ∪ ran
𝑓 ↔ ∪ 𝑡
⊆ ∪ ran 𝑓)) | 
| 156 | 155 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (𝑆 ⊆ ∪ ran
𝑓 ↔ ∪ 𝑡
⊆ ∪ ran 𝑓)) | 
| 157 | 154, 156 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑆 ⊆ ∪ ran
𝑓) | 
| 158 | 116, 157 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓)) | 
| 159 | 158 | ex 412 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓))) | 
| 160 | 159 | eximdv 1917 | . . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓))) | 
| 161 | 160 | ex 412 | . . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓)))) | 
| 162 | 161 | com23 86 | . . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓)))) | 
| 163 |  | unieq 4918 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪
ran 𝑓) | 
| 164 | 163 | sseq2d 4016 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = ran 𝑓 → (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran
𝑓)) | 
| 165 | 164 | rspcev 3622 | . . . . . . . . . . . . . 14
⊢ ((ran
𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) | 
| 166 | 165 | exlimiv 1930 | . . . . . . . . . . . . 13
⊢
(∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) | 
| 167 | 162, 166 | syl8 76 | . . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) | 
| 168 | 97, 167 | mpd 15 | . . . . . . . . . . 11
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) | 
| 169 | 92, 168 | sylan2b 594 | . . . . . . . . . 10
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) | 
| 170 | 169 | rexlimdva 3155 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) | 
| 171 | 81, 170 | biimtrrid 243 | . . . . . . . 8
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) | 
| 172 | 79, 171 | sylbird 260 | . . . . . . 7
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
→ ∃𝑑 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑑)) | 
| 173 | 172 | ex 412 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑆 ⊆ ∪ 𝑐 → ((∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
→ ∃𝑑 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑑))) | 
| 174 | 173 | com23 86 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → ((∪
(𝐽 ↾t
𝑆) = ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
→ (𝑆 ⊆ ∪ 𝑐
→ ∃𝑑 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑑))) | 
| 175 | 53, 174 | syld 47 | . . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) → (𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) | 
| 176 | 175 | ralrimdva 3154 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) | 
| 177 | 4 | cmpsublem 23407 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | 
| 178 | 176, 177 | impbid 212 | . 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) | 
| 179 | 13, 178 | bitrd 279 | 1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |