| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpll 767 | . 2
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Top) | 
| 2 |  | simpll 767 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → 𝐽 ∈ Top) | 
| 3 |  | ssun1 4178 | . . . . . . . . . 10
⊢ 𝑆 ⊆ (𝑆 ∪ 𝑇) | 
| 4 |  | sseq2 4010 | . . . . . . . . . 10
⊢ (𝑋 = (𝑆 ∪ 𝑇) → (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ (𝑆 ∪ 𝑇))) | 
| 5 | 3, 4 | mpbiri 258 | . . . . . . . . 9
⊢ (𝑋 = (𝑆 ∪ 𝑇) → 𝑆 ⊆ 𝑋) | 
| 6 | 5 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → 𝑆 ⊆ 𝑋) | 
| 7 |  | uncmp.1 | . . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 | 
| 8 | 7 | cmpsub 23408 | . . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛))) | 
| 9 | 2, 6, 8 | syl2anc 584 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛))) | 
| 10 |  | simprr 773 | . . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → 𝑋 = ∪ 𝑐) | 
| 11 | 6, 10 | sseqtrd 4020 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → 𝑆 ⊆ ∪ 𝑐) | 
| 12 |  | unieq 4918 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑐 → ∪ 𝑚 = ∪
𝑐) | 
| 13 | 12 | sseq2d 4016 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑐 → (𝑆 ⊆ ∪ 𝑚 ↔ 𝑆 ⊆ ∪ 𝑐)) | 
| 14 |  | pweq 4614 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑐 → 𝒫 𝑚 = 𝒫 𝑐) | 
| 15 | 14 | ineq1d 4219 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑐 → (𝒫 𝑚 ∩ Fin) = (𝒫 𝑐 ∩ Fin)) | 
| 16 | 15 | rexeqdv 3327 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑐 → (∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛 ↔ ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛)) | 
| 17 | 13, 16 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑚 = 𝑐 → ((𝑆 ⊆ ∪ 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛) ↔ (𝑆 ⊆ ∪ 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛))) | 
| 18 | 17 | rspcv 3618 | . . . . . . . . 9
⊢ (𝑐 ∈ 𝒫 𝐽 → (∀𝑚 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛) → (𝑆 ⊆ ∪ 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛))) | 
| 19 | 18 | ad2antrl 728 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛) → (𝑆 ⊆ ∪ 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛))) | 
| 20 | 11, 19 | mpid 44 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 ⊆ ∪ 𝑛) → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛)) | 
| 21 | 9, 20 | sylbid 240 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → ((𝐽 ↾t 𝑆) ∈ Comp → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛)) | 
| 22 |  | ssun2 4179 | . . . . . . . . . 10
⊢ 𝑇 ⊆ (𝑆 ∪ 𝑇) | 
| 23 |  | sseq2 4010 | . . . . . . . . . 10
⊢ (𝑋 = (𝑆 ∪ 𝑇) → (𝑇 ⊆ 𝑋 ↔ 𝑇 ⊆ (𝑆 ∪ 𝑇))) | 
| 24 | 22, 23 | mpbiri 258 | . . . . . . . . 9
⊢ (𝑋 = (𝑆 ∪ 𝑇) → 𝑇 ⊆ 𝑋) | 
| 25 | 24 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → 𝑇 ⊆ 𝑋) | 
| 26 | 7 | cmpsub 23408 | . . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑇 ⊆ 𝑋) → ((𝐽 ↾t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 ⊆ ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠))) | 
| 27 | 2, 25, 26 | syl2anc 584 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → ((𝐽 ↾t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 ⊆ ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠))) | 
| 28 | 25, 10 | sseqtrd 4020 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → 𝑇 ⊆ ∪ 𝑐) | 
| 29 |  | unieq 4918 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑐 → ∪ 𝑟 = ∪
𝑐) | 
| 30 | 29 | sseq2d 4016 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑐 → (𝑇 ⊆ ∪ 𝑟 ↔ 𝑇 ⊆ ∪ 𝑐)) | 
| 31 |  | pweq 4614 | . . . . . . . . . . . . 13
⊢ (𝑟 = 𝑐 → 𝒫 𝑟 = 𝒫 𝑐) | 
| 32 | 31 | ineq1d 4219 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑐 → (𝒫 𝑟 ∩ Fin) = (𝒫 𝑐 ∩ Fin)) | 
| 33 | 32 | rexeqdv 3327 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑐 → (∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠 ↔ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠)) | 
| 34 | 30, 33 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑟 = 𝑐 → ((𝑇 ⊆ ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠) ↔ (𝑇 ⊆ ∪ 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠))) | 
| 35 | 34 | rspcv 3618 | . . . . . . . . 9
⊢ (𝑐 ∈ 𝒫 𝐽 → (∀𝑟 ∈ 𝒫 𝐽(𝑇 ⊆ ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠) → (𝑇 ⊆ ∪ 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠))) | 
| 36 | 35 | ad2antrl 728 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 ⊆ ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠) → (𝑇 ⊆ ∪ 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠))) | 
| 37 | 28, 36 | mpid 44 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 ⊆ ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 ⊆ ∪ 𝑠) → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠)) | 
| 38 | 27, 37 | sylbid 240 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → ((𝐽 ↾t 𝑇) ∈ Comp → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠)) | 
| 39 |  | reeanv 3229 | . . . . . . 7
⊢
(∃𝑛 ∈
(𝒫 𝑐 ∩
Fin)∃𝑠 ∈
(𝒫 𝑐 ∩
Fin)(𝑆 ⊆ ∪ 𝑛
∧ 𝑇 ⊆ ∪ 𝑠)
↔ (∃𝑛 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑛
∧ ∃𝑠 ∈
(𝒫 𝑐 ∩
Fin)𝑇 ⊆ ∪ 𝑠)) | 
| 40 |  | elinel1 4201 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ 𝒫 𝑐) | 
| 41 | 40 | elpwid 4609 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ⊆ 𝑐) | 
| 42 |  | elinel1 4201 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ 𝒫 𝑐) | 
| 43 | 42 | elpwid 4609 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ⊆ 𝑐) | 
| 44 | 41, 43 | anim12i 613 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛 ⊆ 𝑐 ∧ 𝑠 ⊆ 𝑐)) | 
| 45 | 44 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑛 ⊆ 𝑐 ∧ 𝑠 ⊆ 𝑐)) | 
| 46 |  | unss 4190 | . . . . . . . . . . . . 13
⊢ ((𝑛 ⊆ 𝑐 ∧ 𝑠 ⊆ 𝑐) ↔ (𝑛 ∪ 𝑠) ⊆ 𝑐) | 
| 47 | 45, 46 | sylib 218 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑛 ∪ 𝑠) ⊆ 𝑐) | 
| 48 |  | elinel2 4202 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ Fin) | 
| 49 |  | elinel2 4202 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ Fin) | 
| 50 |  | unfi 9211 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ Fin ∧ 𝑠 ∈ Fin) → (𝑛 ∪ 𝑠) ∈ Fin) | 
| 51 | 48, 49, 50 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛 ∪ 𝑠) ∈ Fin) | 
| 52 | 51 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑛 ∪ 𝑠) ∈ Fin) | 
| 53 | 47, 52 | jca 511 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → ((𝑛 ∪ 𝑠) ⊆ 𝑐 ∧ (𝑛 ∪ 𝑠) ∈ Fin)) | 
| 54 |  | elin 3967 | . . . . . . . . . . . 12
⊢ ((𝑛 ∪ 𝑠) ∈ (𝒫 𝑐 ∩ Fin) ↔ ((𝑛 ∪ 𝑠) ∈ 𝒫 𝑐 ∧ (𝑛 ∪ 𝑠) ∈ Fin)) | 
| 55 |  | vex 3484 | . . . . . . . . . . . . . 14
⊢ 𝑐 ∈ V | 
| 56 | 55 | elpw2 5334 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∪ 𝑠) ∈ 𝒫 𝑐 ↔ (𝑛 ∪ 𝑠) ⊆ 𝑐) | 
| 57 | 56 | anbi1i 624 | . . . . . . . . . . . 12
⊢ (((𝑛 ∪ 𝑠) ∈ 𝒫 𝑐 ∧ (𝑛 ∪ 𝑠) ∈ Fin) ↔ ((𝑛 ∪ 𝑠) ⊆ 𝑐 ∧ (𝑛 ∪ 𝑠) ∈ Fin)) | 
| 58 | 54, 57 | bitr2i 276 | . . . . . . . . . . 11
⊢ (((𝑛 ∪ 𝑠) ⊆ 𝑐 ∧ (𝑛 ∪ 𝑠) ∈ Fin) ↔ (𝑛 ∪ 𝑠) ∈ (𝒫 𝑐 ∩ Fin)) | 
| 59 | 53, 58 | sylib 218 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑛 ∪ 𝑠) ∈ (𝒫 𝑐 ∩ Fin)) | 
| 60 |  | simpllr 776 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → 𝑋 = (𝑆 ∪ 𝑇)) | 
| 61 |  | ssun3 4180 | . . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ ∪ 𝑛
→ 𝑆 ⊆ (∪ 𝑛
∪ ∪ 𝑠)) | 
| 62 |  | ssun4 4181 | . . . . . . . . . . . . . . . 16
⊢ (𝑇 ⊆ ∪ 𝑠
→ 𝑇 ⊆ (∪ 𝑛
∪ ∪ 𝑠)) | 
| 63 | 61, 62 | anim12i 613 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ∪ 𝑛
∧ 𝑇 ⊆ ∪ 𝑠)
→ (𝑆 ⊆ (∪ 𝑛
∪ ∪ 𝑠) ∧ 𝑇 ⊆ (∪ 𝑛 ∪ ∪ 𝑠))) | 
| 64 | 63 | ad2antll 729 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑆 ⊆ (∪ 𝑛 ∪ ∪ 𝑠)
∧ 𝑇 ⊆ (∪ 𝑛
∪ ∪ 𝑠))) | 
| 65 |  | unss 4190 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ (∪ 𝑛
∪ ∪ 𝑠) ∧ 𝑇 ⊆ (∪ 𝑛 ∪ ∪ 𝑠))
↔ (𝑆 ∪ 𝑇) ⊆ (∪ 𝑛
∪ ∪ 𝑠)) | 
| 66 | 64, 65 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑆 ∪ 𝑇) ⊆ (∪
𝑛 ∪ ∪ 𝑠)) | 
| 67 | 60, 66 | eqsstrd 4018 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → 𝑋 ⊆ (∪ 𝑛 ∪ ∪ 𝑠)) | 
| 68 |  | uniun 4930 | . . . . . . . . . . . 12
⊢ ∪ (𝑛
∪ 𝑠) = (∪ 𝑛
∪ ∪ 𝑠) | 
| 69 | 67, 68 | sseqtrrdi 4025 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → 𝑋 ⊆ ∪ (𝑛 ∪ 𝑠)) | 
| 70 |  | elpwi 4607 | . . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐) → 𝑐 ⊆ 𝐽) | 
| 72 | 71 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → 𝑐 ⊆ 𝐽) | 
| 73 | 47, 72 | sstrd 3994 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → (𝑛 ∪ 𝑠) ⊆ 𝐽) | 
| 74 |  | uniss 4915 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∪ 𝑠) ⊆ 𝐽 → ∪ (𝑛 ∪ 𝑠) ⊆ ∪ 𝐽) | 
| 75 | 74, 7 | sseqtrrdi 4025 | . . . . . . . . . . . 12
⊢ ((𝑛 ∪ 𝑠) ⊆ 𝐽 → ∪ (𝑛 ∪ 𝑠) ⊆ 𝑋) | 
| 76 | 73, 75 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → ∪ (𝑛
∪ 𝑠) ⊆ 𝑋) | 
| 77 | 69, 76 | eqssd 4001 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → 𝑋 = ∪ (𝑛 ∪ 𝑠)) | 
| 78 |  | unieq 4918 | . . . . . . . . . . 11
⊢ (𝑑 = (𝑛 ∪ 𝑠) → ∪ 𝑑 = ∪
(𝑛 ∪ 𝑠)) | 
| 79 | 78 | rspceeqv 3645 | . . . . . . . . . 10
⊢ (((𝑛 ∪ 𝑠) ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ (𝑛 ∪ 𝑠)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) | 
| 80 | 59, 77, 79 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠))) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) | 
| 81 | 80 | exp32 420 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → ((𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 82 | 81 | rexlimdvv 3212 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 83 | 39, 82 | biimtrrid 243 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → ((∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 ⊆ ∪ 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 84 | 21, 38, 83 | syl2and 608 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐)) → (((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 85 | 84 | impancom 451 | . . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → ((𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 86 | 85 | expd 415 | . . 3
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 87 | 86 | ralrimiv 3145 | . 2
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 88 | 7 | iscmp 23396 | . 2
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 89 | 1, 87, 88 | sylanbrc 583 | 1
⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp) |