| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xkococn.b | . . . 4
⊢ (𝜑 → 𝐵 ∈ (𝑅 Cn 𝑆)) | 
| 2 |  | xkococn.c | . . . 4
⊢ (𝜑 → (𝑅 ↾t 𝐾) ∈ Comp) | 
| 3 |  | imacmp 23406 | . . . 4
⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾t 𝐾) ∈ Comp) → (𝑆 ↾t (𝐵 “ 𝐾)) ∈ Comp) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑆 ↾t (𝐵 “ 𝐾)) ∈ Comp) | 
| 5 |  | xkococn.s | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally
Comp) | 
| 6 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑆 ∈ 𝑛-Locally
Comp) | 
| 7 |  | xkococn.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇)) | 
| 8 |  | xkococn.v | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ 𝑇) | 
| 9 |  | cnima 23274 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (◡𝐴 “ 𝑉) ∈ 𝑆) | 
| 10 | 7, 8, 9 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (◡𝐴 “ 𝑉) ∈ 𝑆) | 
| 11 | 10 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (◡𝐴 “ 𝑉) ∈ 𝑆) | 
| 12 |  | imaco 6270 | . . . . . . . . . . 11
⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾)) | 
| 13 |  | xkococn.i | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉) | 
| 14 | 12, 13 | eqsstrrid 4022 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ ∪ 𝑆 =
∪ 𝑆 | 
| 16 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ ∪ 𝑇 =
∪ 𝑇 | 
| 17 | 15, 16 | cnf 23255 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇) | 
| 18 |  | ffun 6738 | . . . . . . . . . . . 12
⊢ (𝐴:∪
𝑆⟶∪ 𝑇
→ Fun 𝐴) | 
| 19 | 7, 17, 18 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐴) | 
| 20 |  | imassrn 6088 | . . . . . . . . . . . . 13
⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵 | 
| 21 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ∪ 𝑅 =
∪ 𝑅 | 
| 22 | 21, 15 | cnf 23255 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆) | 
| 23 |  | frn 6742 | . . . . . . . . . . . . . 14
⊢ (𝐵:∪
𝑅⟶∪ 𝑆
→ ran 𝐵 ⊆ ∪ 𝑆) | 
| 24 | 1, 22, 23 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆) | 
| 25 | 20, 24 | sstrid 3994 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆) | 
| 26 |  | fdm 6744 | . . . . . . . . . . . . 13
⊢ (𝐴:∪
𝑆⟶∪ 𝑇
→ dom 𝐴 = ∪ 𝑆) | 
| 27 | 7, 17, 26 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐴 = ∪ 𝑆) | 
| 28 | 25, 27 | sseqtrrd 4020 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴) | 
| 29 |  | funimass3 7073 | . . . . . . . . . . 11
⊢ ((Fun
𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (◡𝐴 “ 𝑉))) | 
| 30 | 19, 28, 29 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (◡𝐴 “ 𝑉))) | 
| 31 | 14, 30 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (◡𝐴 “ 𝑉)) | 
| 32 | 31 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (◡𝐴 “ 𝑉)) | 
| 33 |  | nlly2i 23485 | . . . . . . . 8
⊢ ((𝑆 ∈ 𝑛-Locally Comp
∧ (◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp)) | 
| 34 | 6, 11, 32, 33 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp)) | 
| 35 |  | nllytop 23482 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑛-Locally Comp
→ 𝑆 ∈
Top) | 
| 36 | 5, 35 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Top) | 
| 37 | 36 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top) | 
| 38 |  | imaexg 7936 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V) | 
| 39 | 1, 38 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V) | 
| 40 | 39 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V) | 
| 41 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆) | 
| 42 |  | elrestr 17474 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾t (𝐵 “ 𝐾))) | 
| 43 | 37, 40, 41, 42 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾t (𝐵 “ 𝐾))) | 
| 44 |  | simprr1 1221 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢) | 
| 45 |  | simpllr 775 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾)) | 
| 46 | 44, 45 | elind 4199 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))) | 
| 47 |  | inss1 4236 | . . . . . . . . . . . 12
⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢 | 
| 48 |  | elpwi 4606 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉) → 𝑠 ⊆ (◡𝐴 “ 𝑉)) | 
| 49 | 48 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ (◡𝐴 “ 𝑉)) | 
| 50 |  | elssuni 4936 | . . . . . . . . . . . . . . . 16
⊢ ((◡𝐴 “ 𝑉) ∈ 𝑆 → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) | 
| 51 | 10, 50 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) | 
| 52 | 51 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) | 
| 53 | 49, 52 | sstrd 3993 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆) | 
| 54 |  | simprr2 1222 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠) | 
| 55 | 15 | ssntr 23067 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆)
∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠)) | 
| 56 | 37, 53, 41, 54, 55 | syl22anc 838 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠)) | 
| 57 | 47, 56 | sstrid 3994 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠)) | 
| 58 |  | simprr3 1223 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝑆 ↾t 𝑠) ∈ Comp) | 
| 59 | 57, 58 | jca 511 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) | 
| 60 |  | eleq2 2829 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))) | 
| 61 |  | cleq1lem 15022 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 62 | 60, 61 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) | 
| 63 | 62 | rspcev 3621 | . . . . . . . . . 10
⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 64 | 43, 46, 59, 63 | syl12anc 836 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 65 | 64 | rexlimdvaa 3155 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) | 
| 66 | 65 | reximdva 3167 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) | 
| 67 | 34, 66 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 68 |  | rexcom 3289 | . . . . . . 7
⊢
(∃𝑠 ∈
𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 69 |  | r19.42v 3190 | . . . . . . . 8
⊢
(∃𝑠 ∈
𝒫 (◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 70 | 69 | rexbii 3093 | . . . . . . 7
⊢
(∃𝑦 ∈
(𝑆 ↾t
(𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 71 | 68, 70 | bitri 275 | . . . . . 6
⊢
(∃𝑠 ∈
𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 72 | 67, 71 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 73 | 72 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 74 | 15 | restuni 23171 | . . . . 5
⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾t (𝐵 “ 𝐾))) | 
| 75 | 36, 25, 74 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾t (𝐵 “ 𝐾))) | 
| 76 | 73, 75 | raleqtrdv 3327 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) | 
| 77 |  | eqid 2736 | . . . 4
⊢ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ (𝑆
↾t (𝐵
“ 𝐾)) | 
| 78 |  | fveq2 6905 | . . . . . 6
⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 79 | 78 | sseq2d 4015 | . . . . 5
⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))) | 
| 80 |  | oveq2 7440 | . . . . . 6
⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾t 𝑠) = (𝑆 ↾t (𝑘‘𝑦))) | 
| 81 | 80 | eleq1d 2825 | . . . . 5
⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾t 𝑠) ∈ Comp ↔ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) | 
| 82 | 79, 81 | anbi12d 632 | . . . 4
⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp))) | 
| 83 | 77, 82 | cmpcovf 23400 | . . 3
⊢ (((𝑆 ↾t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆
↾t (𝐵
“ 𝐾))∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)(∪
(𝑆 ↾t
(𝐵 “ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) | 
| 84 | 4, 76, 83 | syl2anc 584 | . 2
⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)(∪
(𝑆 ↾t
(𝐵 “ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) | 
| 85 | 75 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾t (𝐵 “ 𝐾))) | 
| 86 | 85 | eqeq1d 2738 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤)) | 
| 87 | 86 | biimpar 477 | . . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤)
→ (𝐵 “ 𝐾) = ∪
𝑤) | 
| 88 | 36 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top) | 
| 89 |  | cntop2 23250 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top) | 
| 90 | 7, 89 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ Top) | 
| 91 | 90 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top) | 
| 92 |  | xkotop 23597 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑ko 𝑆) ∈ Top) | 
| 93 | 88, 91, 92 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ↑ko 𝑆) ∈ Top) | 
| 94 |  | cntop1 23249 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top) | 
| 95 | 1, 94 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Top) | 
| 96 | 95 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top) | 
| 97 |  | xkotop 23597 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top) | 
| 98 | 96, 88, 97 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↑ko 𝑅) ∈ Top) | 
| 99 |  | simprrl 780 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉)) | 
| 100 | 99 | frnd 6743 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (◡𝐴 “ 𝑉)) | 
| 101 |  | sspwuni 5099 | . . . . . . . . . . . 12
⊢ (ran
𝑘 ⊆ 𝒫 (◡𝐴 “ 𝑉) ↔ ∪ ran
𝑘 ⊆ (◡𝐴 “ 𝑉)) | 
| 102 | 100, 101 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (◡𝐴 “ 𝑉)) | 
| 103 | 10 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (◡𝐴 “ 𝑉) ∈ 𝑆) | 
| 104 | 103, 50 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) | 
| 105 | 102, 104 | sstrd 3993 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆) | 
| 106 |  | ffn 6735 | . . . . . . . . . . . . 13
⊢ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤) | 
| 107 |  | fniunfv 7268 | . . . . . . . . . . . . 13
⊢ (𝑘 Fn 𝑤 → ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘) | 
| 108 | 99, 106, 107 | 3syl 18 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘) | 
| 109 | 108 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾t ∪ ran 𝑘)) | 
| 110 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) | 
| 111 | 110 | elin2d 4204 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin) | 
| 112 |  | simprrr 781 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) | 
| 113 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) | 
| 114 | 113 | ralimi 3082 | . . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) | 
| 115 | 112, 114 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) | 
| 116 | 15 | fiuncmp 23413 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp) | 
| 117 | 88, 111, 115, 116 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp) | 
| 118 | 109, 117 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾t ∪ ran 𝑘) ∈ Comp) | 
| 119 | 8 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇) | 
| 120 | 15, 88, 91, 105, 118, 119 | xkoopn 23598 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∈ (𝑇 ↑ko 𝑆)) | 
| 121 |  | xkococn.k | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅) | 
| 122 | 121 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅) | 
| 123 | 2 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾t 𝐾) ∈ Comp) | 
| 124 | 108, 105 | eqsstrd 4017 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆) | 
| 125 |  | iunss 5044 | . . . . . . . . . . . . 13
⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆) | 
| 126 | 124, 125 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆) | 
| 127 | 15 | ntropn 23058 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) | 
| 128 | 127 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)) | 
| 129 | 128 | ralimdv 3168 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Top →
(∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)) | 
| 130 | 88, 126, 129 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) | 
| 131 |  | iunopn 22905 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) | 
| 132 | 88, 130, 131 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) | 
| 133 | 21, 96, 88, 122, 123, 132 | xkoopn 23598 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑ko 𝑅)) | 
| 134 |  | txopn 23611 | . . . . . . . . 9
⊢ ((((𝑇 ↑ko 𝑆) ∈ Top ∧ (𝑆 ↑ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∈ (𝑇 ↑ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))) | 
| 135 | 93, 98, 120, 133, 134 | syl22anc 838 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))) | 
| 136 |  | imaeq1 6072 | . . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran
𝑘) = (𝐴 “ ∪ ran
𝑘)) | 
| 137 | 136 | sseq1d 4014 | . . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran
𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran
𝑘) ⊆ 𝑉)) | 
| 138 | 7 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇)) | 
| 139 |  | imaiun 7266 | . . . . . . . . . . . 12
⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪
𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) | 
| 140 | 108 | imaeq2d 6077 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran
𝑘)) | 
| 141 | 139, 140 | eqtr3id 2790 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran
𝑘)) | 
| 142 | 108, 102 | eqsstrd 4017 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉)) | 
| 143 | 19 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴) | 
| 144 | 99, 106 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤) | 
| 145 | 27 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪
𝑆) | 
| 146 | 105, 145 | sseqtrrd 4020 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴) | 
| 147 |  | simpl1 1191 | . . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴) | 
| 148 | 107 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘) | 
| 149 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran
𝑘 ⊆ dom 𝐴) | 
| 150 | 148, 149 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴) | 
| 151 |  | iunss 5044 | . . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴) | 
| 152 | 150, 151 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴) | 
| 153 | 152 | r19.21bi 3250 | . . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴) | 
| 154 |  | funimass3 7073 | . . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) | 
| 155 | 147, 153,
154 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) | 
| 156 | 155 | ralbidva 3175 | . . . . . . . . . . . . . 14
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) | 
| 157 |  | iunss 5044 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉) | 
| 158 |  | iunss 5044 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉)) | 
| 159 | 156, 157,
158 | 3bitr4g 314 | . . . . . . . . . . . . 13
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) | 
| 160 | 143, 144,
146, 159 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) | 
| 161 | 142, 160 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉) | 
| 162 | 141, 161 | eqsstrrd 4018 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran
𝑘) ⊆ 𝑉) | 
| 163 | 137, 138,
162 | elrabd 3693 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}) | 
| 164 |  | imaeq1 6072 | . . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾)) | 
| 165 | 164 | sseq1d 4014 | . . . . . . . . . 10
⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))) | 
| 166 | 1 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆)) | 
| 167 |  | simprl 770 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤) | 
| 168 |  | uniiun 5057 | . . . . . . . . . . . 12
⊢ ∪ 𝑤 =
∪ 𝑦 ∈ 𝑤 𝑦 | 
| 169 | 167, 168 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪
𝑦 ∈ 𝑤 𝑦) | 
| 170 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 171 | 170 | ralimi 3082 | . . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 172 |  | ss2iun 5009 | . . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪
𝑦 ∈ 𝑤 𝑦 ⊆ ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 173 | 112, 171,
172 | 3syl 18 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 174 | 169, 173 | eqsstrd 4017 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 175 | 165, 166,
174 | elrabd 3693 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) | 
| 176 | 163, 175 | opelxpd 5723 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) | 
| 177 |  | imaeq1 6072 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran
𝑘) = (𝑢 “ ∪ ran
𝑘)) | 
| 178 | 177 | sseq1d 4014 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran
𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉)) | 
| 179 | 178 | elrab 3691 | . . . . . . . . . . . . 13
⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉)) | 
| 180 |  | imaeq1 6072 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾)) | 
| 181 | 180 | sseq1d 4014 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))) | 
| 182 | 181 | elrab 3691 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))) | 
| 183 | 179, 182 | anbi12i 628 | . . . . . . . . . . . 12
⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) | 
| 184 |  | simprll 778 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇)) | 
| 185 |  | simprrl 780 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆)) | 
| 186 |  | coeq1 5867 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑢 → (𝑓 ∘ 𝑔) = (𝑢 ∘ 𝑔)) | 
| 187 |  | coeq2 5868 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑣 → (𝑢 ∘ 𝑔) = (𝑢 ∘ 𝑣)) | 
| 188 |  | xkococn.1 | . . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔)) | 
| 189 |  | vex 3483 | . . . . . . . . . . . . . . . 16
⊢ 𝑢 ∈ V | 
| 190 |  | vex 3483 | . . . . . . . . . . . . . . . 16
⊢ 𝑣 ∈ V | 
| 191 | 189, 190 | coex 7953 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∘ 𝑣) ∈ V | 
| 192 | 186, 187,
188, 191 | ovmpo 7594 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣)) | 
| 193 | 184, 185,
192 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣)) | 
| 194 |  | imaeq1 6072 | . . . . . . . . . . . . . . 15
⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾)) | 
| 195 | 194 | sseq1d 4014 | . . . . . . . . . . . . . 14
⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)) | 
| 196 |  | cnco 23275 | . . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇)) | 
| 197 | 185, 184,
196 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇)) | 
| 198 |  | imaco 6270 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾)) | 
| 199 |  | simprrr 781 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) | 
| 200 | 15 | ntrss2 23066 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)) | 
| 201 | 200 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))) | 
| 202 | 201 | ralimdv 3168 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ∈ Top →
(∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))) | 
| 203 | 88, 126, 202 | sylc 65 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)) | 
| 204 |  | ss2iun 5009 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) | 
| 205 | 203, 204 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) | 
| 206 | 205, 108 | sseqtrd 4019 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran
𝑘) | 
| 207 | 206 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran
𝑘) | 
| 208 | 199, 207 | sstrd 3993 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ ran
𝑘) | 
| 209 |  | imass2 6119 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑣 “ 𝐾) ⊆ ∪ ran
𝑘 → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran
𝑘)) | 
| 210 | 208, 209 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran
𝑘)) | 
| 211 |  | simprlr 779 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) | 
| 212 | 210, 211 | sstrd 3993 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉) | 
| 213 | 198, 212 | eqsstrid 4021 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉) | 
| 214 | 195, 197,
213 | elrabd 3693 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) | 
| 215 | 193, 214 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) | 
| 216 | 183, 215 | sylan2b 594 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) | 
| 217 | 216 | ralrimivva 3201 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) | 
| 218 | 188 | mpofun 7558 | . . . . . . . . . . 11
⊢ Fun 𝐹 | 
| 219 |  | ssrab2 4079 | . . . . . . . . . . . . 13
⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) | 
| 220 |  | ssrab2 4079 | . . . . . . . . . . . . 13
⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆) | 
| 221 |  | xpss12 5699 | . . . . . . . . . . . . 13
⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))) | 
| 222 | 219, 220,
221 | mp2an 692 | . . . . . . . . . . . 12
⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) | 
| 223 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V | 
| 224 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑔 ∈ V | 
| 225 | 223, 224 | coex 7953 | . . . . . . . . . . . . 13
⊢ (𝑓 ∘ 𝑔) ∈ V | 
| 226 | 188, 225 | dmmpo 8097 | . . . . . . . . . . . 12
⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) | 
| 227 | 222, 226 | sseqtrri 4032 | . . . . . . . . . . 11
⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹 | 
| 228 |  | funimassov 7611 | . . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) | 
| 229 | 218, 227,
228 | mp2an 692 | . . . . . . . . . 10
⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) | 
| 230 | 217, 229 | sylibr 234 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) | 
| 231 |  | funimass3 7073 | . . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) | 
| 232 | 218, 227,
231 | mp2an 692 | . . . . . . . . 9
⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) | 
| 233 | 230, 232 | sylib 218 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) | 
| 234 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (〈𝐴, 𝐵〉 ∈ 𝑧 ↔ 〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))) | 
| 235 |  | sseq1 4008 | . . . . . . . . . 10
⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) | 
| 236 | 234, 235 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) | 
| 237 | 236 | rspcev 3621 | . . . . . . . 8
⊢ ((({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅)) ∧ (〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) | 
| 238 | 135, 176,
233, 237 | syl12anc 836 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) | 
| 239 | 238 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → ((𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) | 
| 240 | 239 | exlimdv 1932 | . . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) | 
| 241 | 87, 240 | syldan 591 | . . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤)
→ (∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) | 
| 242 | 241 | expimpd 453 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) → ((∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) | 
| 243 | 242 | rexlimdva 3154 | . 2
⊢ (𝜑 → (∃𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)(∪
(𝑆 ↾t
(𝐵 “ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) | 
| 244 | 84, 243 | mpd 15 | 1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) |