Step | Hyp | Ref
| Expression |
1 | | xkococn.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (𝑅 Cn 𝑆)) |
2 | | xkococn.c |
. . . 4
⊢ (𝜑 → (𝑅 ↾t 𝐾) ∈ Comp) |
3 | | imacmp 22294 |
. . . 4
⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾t 𝐾) ∈ Comp) → (𝑆 ↾t (𝐵 “ 𝐾)) ∈ Comp) |
4 | 1, 2, 3 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑆 ↾t (𝐵 “ 𝐾)) ∈ Comp) |
5 | | xkococn.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally
Comp) |
6 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑆 ∈ 𝑛-Locally
Comp) |
7 | | xkococn.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇)) |
8 | | xkococn.v |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ 𝑇) |
9 | | cnima 22162 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (◡𝐴 “ 𝑉) ∈ 𝑆) |
10 | 7, 8, 9 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐴 “ 𝑉) ∈ 𝑆) |
11 | 10 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (◡𝐴 “ 𝑉) ∈ 𝑆) |
12 | | imaco 6115 |
. . . . . . . . . . 11
⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾)) |
13 | | xkococn.i |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉) |
14 | 12, 13 | eqsstrrid 3950 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉) |
15 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑆 =
∪ 𝑆 |
16 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑇 =
∪ 𝑇 |
17 | 15, 16 | cnf 22143 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇) |
18 | | ffun 6548 |
. . . . . . . . . . . 12
⊢ (𝐴:∪
𝑆⟶∪ 𝑇
→ Fun 𝐴) |
19 | 7, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐴) |
20 | | imassrn 5940 |
. . . . . . . . . . . . 13
⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵 |
21 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑅 =
∪ 𝑅 |
22 | 21, 15 | cnf 22143 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆) |
23 | | frn 6552 |
. . . . . . . . . . . . . 14
⊢ (𝐵:∪
𝑅⟶∪ 𝑆
→ ran 𝐵 ⊆ ∪ 𝑆) |
24 | 1, 22, 23 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆) |
25 | 20, 24 | sstrid 3912 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆) |
26 | | fdm 6554 |
. . . . . . . . . . . . 13
⊢ (𝐴:∪
𝑆⟶∪ 𝑇
→ dom 𝐴 = ∪ 𝑆) |
27 | 7, 17, 26 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐴 = ∪ 𝑆) |
28 | 25, 27 | sseqtrrd 3942 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴) |
29 | | funimass3 6874 |
. . . . . . . . . . 11
⊢ ((Fun
𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (◡𝐴 “ 𝑉))) |
30 | 19, 28, 29 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (◡𝐴 “ 𝑉))) |
31 | 14, 30 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (◡𝐴 “ 𝑉)) |
32 | 31 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (◡𝐴 “ 𝑉)) |
33 | | nlly2i 22373 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑛-Locally Comp
∧ (◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp)) |
34 | 6, 11, 32, 33 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp)) |
35 | | nllytop 22370 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑛-Locally Comp
→ 𝑆 ∈
Top) |
36 | 5, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Top) |
37 | 36 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top) |
38 | | imaexg 7693 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V) |
39 | 1, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V) |
40 | 39 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V) |
41 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆) |
42 | | elrestr 16933 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾t (𝐵 “ 𝐾))) |
43 | 37, 40, 41, 42 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾t (𝐵 “ 𝐾))) |
44 | | simprr1 1223 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢) |
45 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾)) |
46 | 44, 45 | elind 4108 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))) |
47 | | inss1 4143 |
. . . . . . . . . . . 12
⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢 |
48 | | elpwi 4522 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉) → 𝑠 ⊆ (◡𝐴 “ 𝑉)) |
49 | 48 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ (◡𝐴 “ 𝑉)) |
50 | | elssuni 4851 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐴 “ 𝑉) ∈ 𝑆 → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) |
51 | 10, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) |
52 | 51 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) |
53 | 49, 52 | sstrd 3911 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆) |
54 | | simprr2 1224 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠) |
55 | 15 | ssntr 21955 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆)
∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠)) |
56 | 37, 53, 41, 54, 55 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠)) |
57 | 47, 56 | sstrid 3912 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠)) |
58 | | simprr3 1225 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → (𝑆 ↾t 𝑠) ∈ Comp) |
59 | 57, 58 | jca 515 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) |
60 | | eleq2 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))) |
61 | | cleq1lem 14545 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
62 | 60, 61 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) |
63 | 62 | rspcev 3537 |
. . . . . . . . . 10
⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
64 | 43, 46, 59, 63 | syl12anc 837 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
65 | 64 | rexlimdvaa 3204 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) |
66 | 65 | reximdva 3193 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) |
67 | 34, 66 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
68 | | rexcom 3268 |
. . . . . . 7
⊢
(∃𝑠 ∈
𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
69 | | r19.42v 3263 |
. . . . . . . 8
⊢
(∃𝑠 ∈
𝒫 (◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
70 | 69 | rexbii 3170 |
. . . . . . 7
⊢
(∃𝑦 ∈
(𝑆 ↾t
(𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
71 | 68, 70 | bitri 278 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 (◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
72 | 67, 71 | sylib 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
73 | 72 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
74 | 15 | restuni 22059 |
. . . . . 6
⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾t (𝐵 “ 𝐾))) |
75 | 36, 25, 74 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾t (𝐵 “ 𝐾))) |
76 | 75 | raleqdv 3325 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)) ↔ ∀𝑥 ∈ ∪ (𝑆
↾t (𝐵
“ 𝐾))∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp)))) |
77 | 73, 76 | mpbid 235 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) |
78 | | eqid 2737 |
. . . 4
⊢ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ (𝑆
↾t (𝐵
“ 𝐾)) |
79 | | fveq2 6717 |
. . . . . 6
⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦))) |
80 | 79 | sseq2d 3933 |
. . . . 5
⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))) |
81 | | oveq2 7221 |
. . . . . 6
⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾t 𝑠) = (𝑆 ↾t (𝑘‘𝑦))) |
82 | 81 | eleq1d 2822 |
. . . . 5
⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾t 𝑠) ∈ Comp ↔ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) |
83 | 80, 82 | anbi12d 634 |
. . . 4
⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp))) |
84 | 78, 83 | cmpcovf 22288 |
. . 3
⊢ (((𝑆 ↾t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆
↾t (𝐵
“ 𝐾))∃𝑦 ∈ (𝑆 ↾t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)(∪
(𝑆 ↾t
(𝐵 “ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) |
85 | 4, 77, 84 | syl2anc 587 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)(∪
(𝑆 ↾t
(𝐵 “ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) |
86 | 75 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾t (𝐵 “ 𝐾))) |
87 | 86 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤)) |
88 | 87 | biimpar 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤)
→ (𝐵 “ 𝐾) = ∪
𝑤) |
89 | 36 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top) |
90 | | cntop2 22138 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top) |
91 | 7, 90 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ Top) |
92 | 91 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top) |
93 | | xkotop 22485 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑ko 𝑆) ∈ Top) |
94 | 89, 92, 93 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ↑ko 𝑆) ∈ Top) |
95 | | cntop1 22137 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top) |
96 | 1, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Top) |
97 | 96 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top) |
98 | | xkotop 22485 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top) |
99 | 97, 89, 98 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↑ko 𝑅) ∈ Top) |
100 | | simprrl 781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉)) |
101 | 100 | frnd 6553 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (◡𝐴 “ 𝑉)) |
102 | | sspwuni 5008 |
. . . . . . . . . . . 12
⊢ (ran
𝑘 ⊆ 𝒫 (◡𝐴 “ 𝑉) ↔ ∪ ran
𝑘 ⊆ (◡𝐴 “ 𝑉)) |
103 | 101, 102 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (◡𝐴 “ 𝑉)) |
104 | 10 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (◡𝐴 “ 𝑉) ∈ 𝑆) |
105 | 104, 50 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (◡𝐴 “ 𝑉) ⊆ ∪ 𝑆) |
106 | 103, 105 | sstrd 3911 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆) |
107 | | ffn 6545 |
. . . . . . . . . . . . 13
⊢ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤) |
108 | | fniunfv 7060 |
. . . . . . . . . . . . 13
⊢ (𝑘 Fn 𝑤 → ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘) |
109 | 100, 107,
108 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘) |
110 | 109 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾t ∪ ran 𝑘)) |
111 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) |
112 | 111 | elin2d 4113 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin) |
113 | | simprrr 782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) |
114 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) |
115 | 114 | ralimi 3083 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) |
116 | 113, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) |
117 | 15 | fiuncmp 22301 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp) |
118 | 89, 112, 116, 117 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp) |
119 | 110, 118 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾t ∪ ran 𝑘) ∈ Comp) |
120 | 8 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇) |
121 | 15, 89, 92, 106, 119, 120 | xkoopn 22486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∈ (𝑇 ↑ko 𝑆)) |
122 | | xkococn.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅) |
123 | 122 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅) |
124 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾t 𝐾) ∈ Comp) |
125 | 109, 106 | eqsstrd 3939 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆) |
126 | | iunss 4954 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆) |
127 | 125, 126 | sylib 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆) |
128 | 15 | ntropn 21946 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) |
129 | 128 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)) |
130 | 129 | ralimdv 3101 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Top →
(∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)) |
131 | 89, 127, 130 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) |
132 | | iunopn 21795 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) |
133 | 89, 131, 132 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) |
134 | 21, 97, 89, 123, 124, 133 | xkoopn 22486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑ko 𝑅)) |
135 | | txopn 22499 |
. . . . . . . . 9
⊢ ((((𝑇 ↑ko 𝑆) ∈ Top ∧ (𝑆 ↑ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∈ (𝑇 ↑ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))) |
136 | 94, 99, 121, 134, 135 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))) |
137 | | imaeq1 5924 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran
𝑘) = (𝐴 “ ∪ ran
𝑘)) |
138 | 137 | sseq1d 3932 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran
𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran
𝑘) ⊆ 𝑉)) |
139 | 7 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇)) |
140 | | imaiun 7058 |
. . . . . . . . . . . 12
⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪
𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) |
141 | 109 | imaeq2d 5929 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran
𝑘)) |
142 | 140, 141 | eqtr3id 2792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran
𝑘)) |
143 | 109, 103 | eqsstrd 3939 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉)) |
144 | 19 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴) |
145 | 100, 107 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤) |
146 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪
𝑆) |
147 | 106, 146 | sseqtrrd 3942 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴) |
148 | | simpl1 1193 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴) |
149 | 108 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘) |
150 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran
𝑘 ⊆ dom 𝐴) |
151 | 149, 150 | eqsstrd 3939 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴) |
152 | | iunss 4954 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴) |
153 | 151, 152 | sylib 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴) |
154 | 153 | r19.21bi 3130 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴) |
155 | | funimass3 6874 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) |
156 | 148, 154,
155 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) |
157 | 156 | ralbidva 3117 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) |
158 | | iunss 4954 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉) |
159 | | iunss 4954 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉)) |
160 | 157, 158,
159 | 3bitr4g 317 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) |
161 | 144, 145,
147, 160 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪
𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (◡𝐴 “ 𝑉))) |
162 | 143, 161 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉) |
163 | 142, 162 | eqsstrrd 3940 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran
𝑘) ⊆ 𝑉) |
164 | 138, 139,
163 | elrabd 3604 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}) |
165 | | imaeq1 5924 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾)) |
166 | 165 | sseq1d 3932 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))) |
167 | 1 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆)) |
168 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤) |
169 | | uniiun 4967 |
. . . . . . . . . . . 12
⊢ ∪ 𝑤 =
∪ 𝑦 ∈ 𝑤 𝑦 |
170 | 168, 169 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪
𝑦 ∈ 𝑤 𝑦) |
171 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))) |
172 | 171 | ralimi 3083 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))) |
173 | | ss2iun 4922 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪
𝑦 ∈ 𝑤 𝑦 ⊆ ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) |
174 | 113, 172,
173 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) |
175 | 170, 174 | eqsstrd 3939 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) |
176 | 166, 167,
175 | elrabd 3604 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) |
177 | 164, 176 | opelxpd 5589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → 〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) |
178 | | imaeq1 5924 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran
𝑘) = (𝑢 “ ∪ ran
𝑘)) |
179 | 178 | sseq1d 3932 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran
𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉)) |
180 | 179 | elrab 3602 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉)) |
181 | | imaeq1 5924 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾)) |
182 | 181 | sseq1d 3932 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))) |
183 | 182 | elrab 3602 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))) |
184 | 180, 183 | anbi12i 630 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) |
185 | | simprll 779 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇)) |
186 | | simprrl 781 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆)) |
187 | | coeq1 5726 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑢 → (𝑓 ∘ 𝑔) = (𝑢 ∘ 𝑔)) |
188 | | coeq2 5727 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑣 → (𝑢 ∘ 𝑔) = (𝑢 ∘ 𝑣)) |
189 | | xkococn.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔)) |
190 | | vex 3412 |
. . . . . . . . . . . . . . . 16
⊢ 𝑢 ∈ V |
191 | | vex 3412 |
. . . . . . . . . . . . . . . 16
⊢ 𝑣 ∈ V |
192 | 190, 191 | coex 7708 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∘ 𝑣) ∈ V |
193 | 187, 188,
189, 192 | ovmpo 7369 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣)) |
194 | 185, 186,
193 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣)) |
195 | | imaeq1 5924 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾)) |
196 | 195 | sseq1d 3932 |
. . . . . . . . . . . . . 14
⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)) |
197 | | cnco 22163 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇)) |
198 | 186, 185,
197 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇)) |
199 | | imaco 6115 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾)) |
200 | | simprrr 782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))) |
201 | 15 | ntrss2 21954 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)) |
202 | 201 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))) |
203 | 202 | ralimdv 3101 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ∈ Top →
(∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))) |
204 | 89, 127, 203 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)) |
205 | | ss2iun 4922 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪
𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) |
207 | 206, 109 | sseqtrd 3941 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran
𝑘) |
208 | 207 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran
𝑘) |
209 | 200, 208 | sstrd 3911 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ ran
𝑘) |
210 | | imass2 5970 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 “ 𝐾) ⊆ ∪ ran
𝑘 → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran
𝑘)) |
211 | 209, 210 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran
𝑘)) |
212 | | simprlr 780 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) |
213 | 211, 212 | sstrd 3911 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉) |
214 | 199, 213 | eqsstrid 3949 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉) |
215 | 196, 198,
214 | elrabd 3604 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) |
216 | 194, 215 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran
𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) |
217 | 184, 216 | sylan2b 597 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) |
218 | 217 | ralrimivva 3112 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) |
219 | 189 | mpofun 7334 |
. . . . . . . . . . 11
⊢ Fun 𝐹 |
220 | | ssrab2 3993 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) |
221 | | ssrab2 3993 |
. . . . . . . . . . . . 13
⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆) |
222 | | xpss12 5566 |
. . . . . . . . . . . . 13
⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))) |
223 | 220, 221,
222 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) |
224 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
225 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑔 ∈ V |
226 | 224, 225 | coex 7708 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∘ 𝑔) ∈ V |
227 | 189, 226 | dmmpo 7841 |
. . . . . . . . . . . 12
⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) |
228 | 223, 227 | sseqtrri 3938 |
. . . . . . . . . . 11
⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹 |
229 | | funimassov 7385 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) |
230 | 219, 228,
229 | mp2an 692 |
. . . . . . . . . 10
⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) |
231 | 218, 230 | sylibr 237 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) |
232 | | funimass3 6874 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) |
233 | 219, 228,
232 | mp2an 692 |
. . . . . . . . 9
⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) |
234 | 231, 233 | sylib 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) |
235 | | eleq2 2826 |
. . . . . . . . . 10
⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (〈𝐴, 𝐵〉 ∈ 𝑧 ↔ 〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))) |
236 | | sseq1 3926 |
. . . . . . . . . 10
⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) |
237 | 235, 236 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) |
238 | 237 | rspcev 3537 |
. . . . . . . 8
⊢ ((({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅)) ∧ (〈𝐴, 𝐵〉 ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran
𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) |
239 | 136, 177,
234, 238 | syl12anc 837 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) |
240 | 239 | expr 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → ((𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) |
241 | 240 | exlimdv 1941 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) |
242 | 88, 241 | syldan 594 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤)
→ (∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) |
243 | 242 | expimpd 457 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)) → ((∪ (𝑆
↾t (𝐵
“ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) |
244 | 243 | rexlimdva 3203 |
. 2
⊢ (𝜑 → (∃𝑤 ∈ (𝒫 (𝑆 ↾t (𝐵 “ 𝐾)) ∩ Fin)(∪
(𝑆 ↾t
(𝐵 “ 𝐾)) = ∪ 𝑤
∧ ∃𝑘(𝑘:𝑤⟶𝒫 (◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))) |
245 | 85, 244 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) |