Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkococnlem Structured version   Visualization version   GIF version

Theorem xkococnlem 22271
 Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
xkococn.1 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓𝑔))
xkococn.s (𝜑𝑆 ∈ 𝑛-Locally Comp)
xkococn.k (𝜑𝐾 𝑅)
xkococn.c (𝜑 → (𝑅t 𝐾) ∈ Comp)
xkococn.v (𝜑𝑉𝑇)
xkococn.a (𝜑𝐴 ∈ (𝑆 Cn 𝑇))
xkococn.b (𝜑𝐵 ∈ (𝑅 Cn 𝑆))
xkococn.i (𝜑 → ((𝐴𝐵) “ 𝐾) ⊆ 𝑉)
Assertion
Ref Expression
xkococnlem (𝜑 → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐵   𝑓,𝑔,,𝑧,𝑅   𝑆,𝑓,𝑔,𝑧   ,𝐾,𝑧   𝑇,𝑓,𝑔,,𝑧   𝑧,𝐹   ,𝑉,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑓,𝑔,)   𝐴(𝑓,𝑔,)   𝐵(𝑓,𝑔,)   𝑆()   𝐹(𝑓,𝑔,)   𝐾(𝑓,𝑔)   𝑉(𝑓,𝑔)

Proof of Theorem xkococnlem
Dummy variables 𝑘 𝑎 𝑠 𝑢 𝑣 𝑤 𝑥 𝑦 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkococn.b . . . 4 (𝜑𝐵 ∈ (𝑅 Cn 𝑆))
2 xkococn.c . . . 4 (𝜑 → (𝑅t 𝐾) ∈ Comp)
3 imacmp 22009 . . . 4 ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅t 𝐾) ∈ Comp) → (𝑆t (𝐵𝐾)) ∈ Comp)
41, 2, 3syl2anc 587 . . 3 (𝜑 → (𝑆t (𝐵𝐾)) ∈ Comp)
5 xkococn.s . . . . . . . . 9 (𝜑𝑆 ∈ 𝑛-Locally Comp)
65adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → 𝑆 ∈ 𝑛-Locally Comp)
7 xkococn.a . . . . . . . . . 10 (𝜑𝐴 ∈ (𝑆 Cn 𝑇))
8 xkococn.v . . . . . . . . . 10 (𝜑𝑉𝑇)
9 cnima 21877 . . . . . . . . . 10 ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉𝑇) → (𝐴𝑉) ∈ 𝑆)
107, 8, 9syl2anc 587 . . . . . . . . 9 (𝜑 → (𝐴𝑉) ∈ 𝑆)
1110adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → (𝐴𝑉) ∈ 𝑆)
12 imaco 6071 . . . . . . . . . . 11 ((𝐴𝐵) “ 𝐾) = (𝐴 “ (𝐵𝐾))
13 xkococn.i . . . . . . . . . . 11 (𝜑 → ((𝐴𝐵) “ 𝐾) ⊆ 𝑉)
1412, 13eqsstrrid 3964 . . . . . . . . . 10 (𝜑 → (𝐴 “ (𝐵𝐾)) ⊆ 𝑉)
15 eqid 2798 . . . . . . . . . . . . 13 𝑆 = 𝑆
16 eqid 2798 . . . . . . . . . . . . 13 𝑇 = 𝑇
1715, 16cnf 21858 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴: 𝑆 𝑇)
18 ffun 6490 . . . . . . . . . . . 12 (𝐴: 𝑆 𝑇 → Fun 𝐴)
197, 17, 183syl 18 . . . . . . . . . . 11 (𝜑 → Fun 𝐴)
20 imassrn 5907 . . . . . . . . . . . . 13 (𝐵𝐾) ⊆ ran 𝐵
21 eqid 2798 . . . . . . . . . . . . . . 15 𝑅 = 𝑅
2221, 15cnf 21858 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵: 𝑅 𝑆)
23 frn 6493 . . . . . . . . . . . . . 14 (𝐵: 𝑅 𝑆 → ran 𝐵 𝑆)
241, 22, 233syl 18 . . . . . . . . . . . . 13 (𝜑 → ran 𝐵 𝑆)
2520, 24sstrid 3926 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐾) ⊆ 𝑆)
26 fdm 6495 . . . . . . . . . . . . 13 (𝐴: 𝑆 𝑇 → dom 𝐴 = 𝑆)
277, 17, 263syl 18 . . . . . . . . . . . 12 (𝜑 → dom 𝐴 = 𝑆)
2825, 27sseqtrrd 3956 . . . . . . . . . . 11 (𝜑 → (𝐵𝐾) ⊆ dom 𝐴)
29 funimass3 6801 . . . . . . . . . . 11 ((Fun 𝐴 ∧ (𝐵𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵𝐾)) ⊆ 𝑉 ↔ (𝐵𝐾) ⊆ (𝐴𝑉)))
3019, 28, 29syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝐴 “ (𝐵𝐾)) ⊆ 𝑉 ↔ (𝐵𝐾) ⊆ (𝐴𝑉)))
3114, 30mpbid 235 . . . . . . . . 9 (𝜑 → (𝐵𝐾) ⊆ (𝐴𝑉))
3231sselda 3915 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → 𝑥 ∈ (𝐴𝑉))
33 nlly2i 22088 . . . . . . . 8 ((𝑆 ∈ 𝑛-Locally Comp ∧ (𝐴𝑉) ∈ 𝑆𝑥 ∈ (𝐴𝑉)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))
346, 11, 32, 33syl3anc 1368 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))
35 nllytop 22085 . . . . . . . . . . . . 13 (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
365, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Top)
3736ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38 imaexg 7604 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵𝐾) ∈ V)
391, 38syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐾) ∈ V)
4039ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝐵𝐾) ∈ V)
41 simprl 770 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢𝑆)
42 elrestr 16696 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ (𝐵𝐾) ∈ V ∧ 𝑢𝑆) → (𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)))
4337, 40, 41, 42syl3anc 1368 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)))
44 simprr1 1218 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥𝑢)
45 simpllr 775 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵𝐾))
4644, 45elind 4121 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵𝐾)))
47 inss1 4155 . . . . . . . . . . . 12 (𝑢 ∩ (𝐵𝐾)) ⊆ 𝑢
48 elpwi 4506 . . . . . . . . . . . . . . 15 (𝑠 ∈ 𝒫 (𝐴𝑉) → 𝑠 ⊆ (𝐴𝑉))
4948ad2antlr 726 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑠 ⊆ (𝐴𝑉))
50 elssuni 4830 . . . . . . . . . . . . . . . 16 ((𝐴𝑉) ∈ 𝑆 → (𝐴𝑉) ⊆ 𝑆)
5110, 50syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝑉) ⊆ 𝑆)
5251ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝐴𝑉) ⊆ 𝑆)
5349, 52sstrd 3925 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑠 𝑆)
54 simprr2 1219 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢𝑠)
5515ssntr 21670 . . . . . . . . . . . . 13 (((𝑆 ∈ Top ∧ 𝑠 𝑆) ∧ (𝑢𝑆𝑢𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
5637, 53, 41, 54, 55syl22anc 837 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
5747, 56sstrid 3926 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58 simprr3 1220 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑆t 𝑠) ∈ Comp)
5957, 58jca 515 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))
60 eleq2 2878 . . . . . . . . . . . 12 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → (𝑥𝑦𝑥 ∈ (𝑢 ∩ (𝐵𝐾))))
61 cleq1lem 14335 . . . . . . . . . . . 12 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6260, 61anbi12d 633 . . . . . . . . . . 11 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → ((𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵𝐾)) ∧ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6362rspcev 3571 . . . . . . . . . 10 (((𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵𝐾)) ∧ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6443, 46, 59, 63syl12anc 835 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6564rexlimdvaa 3244 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) → (∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6665reximdva 3233 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵𝐾)) → (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6734, 66mpd 15 . . . . . 6 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
68 rexcom 3308 . . . . . . 7 (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
69 r19.42v 3303 . . . . . . . 8 (∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ (𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7069rexbii 3210 . . . . . . 7 (∃𝑦 ∈ (𝑆t (𝐵𝐾))∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7168, 70bitri 278 . . . . . 6 (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7267, 71sylib 221 . . . . 5 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7372ralrimiva 3149 . . . 4 (𝜑 → ∀𝑥 ∈ (𝐵𝐾)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7415restuni 21774 . . . . . 6 ((𝑆 ∈ Top ∧ (𝐵𝐾) ⊆ 𝑆) → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
7536, 25, 74syl2anc 587 . . . . 5 (𝜑 → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
7675raleqdv 3364 . . . 4 (𝜑 → (∀𝑥 ∈ (𝐵𝐾)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
7773, 76mpbid 235 . . 3 (𝜑 → ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
78 eqid 2798 . . . 4 (𝑆t (𝐵𝐾)) = (𝑆t (𝐵𝐾))
79 fveq2 6645 . . . . . 6 (𝑠 = (𝑘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘𝑦)))
8079sseq2d 3947 . . . . 5 (𝑠 = (𝑘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦))))
81 oveq2 7143 . . . . . 6 (𝑠 = (𝑘𝑦) → (𝑆t 𝑠) = (𝑆t (𝑘𝑦)))
8281eleq1d 2874 . . . . 5 (𝑠 = (𝑘𝑦) → ((𝑆t 𝑠) ∈ Comp ↔ (𝑆t (𝑘𝑦)) ∈ Comp))
8380, 82anbi12d 633 . . . 4 (𝑠 = (𝑘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))
8478, 83cmpcovf 22003 . . 3 (((𝑆t (𝐵𝐾)) ∈ Comp ∧ ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))))
854, 77, 84syl2anc 587 . 2 (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))))
8675adantr 484 . . . . . . 7 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
8786eqeq1d 2800 . . . . . 6 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → ((𝐵𝐾) = 𝑤 (𝑆t (𝐵𝐾)) = 𝑤))
8887biimpar 481 . . . . 5 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝑆t (𝐵𝐾)) = 𝑤) → (𝐵𝐾) = 𝑤)
8936ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
90 cntop2 21853 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
917, 90syl 17 . . . . . . . . . . 11 (𝜑𝑇 ∈ Top)
9291ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
93 xkotop 22200 . . . . . . . . . 10 ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇ko 𝑆) ∈ Top)
9489, 92, 93syl2anc 587 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑇ko 𝑆) ∈ Top)
95 cntop1 21852 . . . . . . . . . . . 12 (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
961, 95syl 17 . . . . . . . . . . 11 (𝜑𝑅 ∈ Top)
9796ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
98 xkotop 22200 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ Top)
9997, 89, 98syl2anc 587 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆ko 𝑅) ∈ Top)
100 simprrl 780 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (𝐴𝑉))
101100frnd 6494 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (𝐴𝑉))
102 sspwuni 4985 . . . . . . . . . . . 12 (ran 𝑘 ⊆ 𝒫 (𝐴𝑉) ↔ ran 𝑘 ⊆ (𝐴𝑉))
103101, 102sylib 221 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ (𝐴𝑉))
10410ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴𝑉) ∈ 𝑆)
105104, 50syl 17 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴𝑉) ⊆ 𝑆)
106103, 105sstrd 3925 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 𝑆)
107 ffn 6487 . . . . . . . . . . . . 13 (𝑘:𝑤⟶𝒫 (𝐴𝑉) → 𝑘 Fn 𝑤)
108 fniunfv 6984 . . . . . . . . . . . . 13 (𝑘 Fn 𝑤 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
109100, 107, 1083syl 18 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
110109oveq2d 7151 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t 𝑦𝑤 (𝑘𝑦)) = (𝑆t ran 𝑘))
111 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin))
112111elin2d 4126 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
113 simprrr 781 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))
114 simpr 488 . . . . . . . . . . . . . 14 ((𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → (𝑆t (𝑘𝑦)) ∈ Comp)
115114ralimi 3128 . . . . . . . . . . . . 13 (∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp)
116113, 115syl 17 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp)
11715fiuncmp 22016 . . . . . . . . . . . 12 ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp) → (𝑆t 𝑦𝑤 (𝑘𝑦)) ∈ Comp)
11889, 112, 116, 117syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t 𝑦𝑤 (𝑘𝑦)) ∈ Comp)
119110, 118eqeltrrd 2891 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t ran 𝑘) ∈ Comp)
1208ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑉𝑇)
12115, 89, 92, 106, 119, 120xkoopn 22201 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∈ (𝑇ko 𝑆))
122 xkococn.k . . . . . . . . . . 11 (𝜑𝐾 𝑅)
123122ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐾 𝑅)
1242ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑅t 𝐾) ∈ Comp)
125109, 106eqsstrd 3953 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
126 iunss 4932 . . . . . . . . . . . . 13 ( 𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
127125, 126sylib 221 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
12815ntropn 21661 . . . . . . . . . . . . . 14 ((𝑆 ∈ Top ∧ (𝑘𝑦) ⊆ 𝑆) → ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
129128ex 416 . . . . . . . . . . . . 13 (𝑆 ∈ Top → ((𝑘𝑦) ⊆ 𝑆 → ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆))
130129ralimdv 3145 . . . . . . . . . . . 12 (𝑆 ∈ Top → (∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆))
13189, 127, 130sylc 65 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
132 iunopn 21510 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
13389, 131, 132syl2anc 587 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
13421, 97, 89, 123, 124, 133xkoopn 22201 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ∈ (𝑆ko 𝑅))
135 txopn 22214 . . . . . . . . 9 ((((𝑇ko 𝑆) ∈ Top ∧ (𝑆ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∈ (𝑇ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ∈ (𝑆ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅)))
13694, 99, 121, 134, 135syl22anc 837 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅)))
137 imaeq1 5891 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 ran 𝑘) = (𝐴 ran 𝑘))
138137sseq1d 3946 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑎 ran 𝑘) ⊆ 𝑉 ↔ (𝐴 ran 𝑘) ⊆ 𝑉))
1397ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
140 imaiun 6982 . . . . . . . . . . . 12 (𝐴 𝑦𝑤 (𝑘𝑦)) = 𝑦𝑤 (𝐴 “ (𝑘𝑦))
141109imaeq2d 5896 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴 𝑦𝑤 (𝑘𝑦)) = (𝐴 ran 𝑘))
142140, 141syl5eqr 2847 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝐴 “ (𝑘𝑦)) = (𝐴 ran 𝑘))
143109, 103eqsstrd 3953 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉))
14419ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → Fun 𝐴)
145100, 107syl 17 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
14627ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → dom 𝐴 = 𝑆)
147106, 146sseqtrrd 3956 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ dom 𝐴)
148 simpl1 1188 . . . . . . . . . . . . . . . 16 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → Fun 𝐴)
1491083ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
150 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ran 𝑘 ⊆ dom 𝐴)
151149, 150eqsstrd 3953 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → 𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
152 iunss 4932 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
153151, 152sylib 221 . . . . . . . . . . . . . . . . 17 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ∀𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
154153r19.21bi 3173 . . . . . . . . . . . . . . . 16 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → (𝑘𝑦) ⊆ dom 𝐴)
155 funimass3 6801 . . . . . . . . . . . . . . . 16 ((Fun 𝐴 ∧ (𝑘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ (𝑘𝑦) ⊆ (𝐴𝑉)))
156148, 154, 155syl2anc 587 . . . . . . . . . . . . . . 15 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → ((𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ (𝑘𝑦) ⊆ (𝐴𝑉)))
157156ralbidva 3161 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → (∀𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
158 iunss 4932 . . . . . . . . . . . . . 14 ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ ∀𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉)
159 iunss 4932 . . . . . . . . . . . . . 14 ( 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉) ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉))
160157, 158, 1593bitr4g 317 . . . . . . . . . . . . 13 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
161144, 145, 147, 160syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
162143, 161mpbird 260 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉)
163142, 162eqsstrrd 3954 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴 ran 𝑘) ⊆ 𝑉)
164138, 139, 163elrabd 3630 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉})
165 imaeq1 5891 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏𝐾) = (𝐵𝐾))
166165sseq1d 3946 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ↔ (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
1671ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
168 simprl 770 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) = 𝑤)
169 uniiun 4945 . . . . . . . . . . . 12 𝑤 = 𝑦𝑤 𝑦
170168, 169eqtrdi 2849 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) = 𝑦𝑤 𝑦)
171 simpl 486 . . . . . . . . . . . . 13 ((𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)))
172171ralimi 3128 . . . . . . . . . . . 12 (∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → ∀𝑦𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)))
173 ss2iun 4899 . . . . . . . . . . . 12 (∀𝑦𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) → 𝑦𝑤 𝑦 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
174113, 172, 1733syl 18 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 𝑦 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
175170, 174eqsstrd 3953 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
176166, 167, 175elrabd 3630 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})
177164, 176opelxpd 5557 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}))
178 imaeq1 5891 . . . . . . . . . . . . . . 15 (𝑎 = 𝑢 → (𝑎 ran 𝑘) = (𝑢 ran 𝑘))
179178sseq1d 3946 . . . . . . . . . . . . . 14 (𝑎 = 𝑢 → ((𝑎 ran 𝑘) ⊆ 𝑉 ↔ (𝑢 ran 𝑘) ⊆ 𝑉))
180179elrab 3628 . . . . . . . . . . . . 13 (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉))
181 imaeq1 5891 . . . . . . . . . . . . . . 15 (𝑏 = 𝑣 → (𝑏𝐾) = (𝑣𝐾))
182181sseq1d 3946 . . . . . . . . . . . . . 14 (𝑏 = 𝑣 → ((𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ↔ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
183182elrab 3628 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
184180, 183anbi12i 629 . . . . . . . . . . . 12 ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))))
185 simprll 778 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
186 simprrl 780 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
187 coeq1 5692 . . . . . . . . . . . . . . 15 (𝑓 = 𝑢 → (𝑓𝑔) = (𝑢𝑔))
188 coeq2 5693 . . . . . . . . . . . . . . 15 (𝑔 = 𝑣 → (𝑢𝑔) = (𝑢𝑣))
189 xkococn.1 . . . . . . . . . . . . . . 15 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓𝑔))
190 vex 3444 . . . . . . . . . . . . . . . 16 𝑢 ∈ V
191 vex 3444 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
192190, 191coex 7619 . . . . . . . . . . . . . . 15 (𝑢𝑣) ∈ V
193187, 188, 189, 192ovmpo 7290 . . . . . . . . . . . . . 14 ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢𝑣))
194185, 186, 193syl2anc 587 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝐹𝑣) = (𝑢𝑣))
195 imaeq1 5891 . . . . . . . . . . . . . . 15 ( = (𝑢𝑣) → (𝐾) = ((𝑢𝑣) “ 𝐾))
196195sseq1d 3946 . . . . . . . . . . . . . 14 ( = (𝑢𝑣) → ((𝐾) ⊆ 𝑉 ↔ ((𝑢𝑣) “ 𝐾) ⊆ 𝑉))
197 cnco 21878 . . . . . . . . . . . . . . 15 ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢𝑣) ∈ (𝑅 Cn 𝑇))
198186, 185, 197syl2anc 587 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝑣) ∈ (𝑅 Cn 𝑇))
199 imaco 6071 . . . . . . . . . . . . . . 15 ((𝑢𝑣) “ 𝐾) = (𝑢 “ (𝑣𝐾))
200 simprrr 781 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
20115ntrss2 21669 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ Top ∧ (𝑘𝑦) ⊆ 𝑆) → ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦))
202201ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ Top → ((𝑘𝑦) ⊆ 𝑆 → ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦)))
203202ralimdv 3145 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ Top → (∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦)))
20489, 127, 203sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦))
205 ss2iun 4899 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ 𝑦𝑤 (𝑘𝑦))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ 𝑦𝑤 (𝑘𝑦))
207206, 109sseqtrd 3955 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ ran 𝑘)
208207adantr 484 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ ran 𝑘)
209200, 208sstrd 3925 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑣𝐾) ⊆ ran 𝑘)
210 imass2 5932 . . . . . . . . . . . . . . . . 17 ((𝑣𝐾) ⊆ ran 𝑘 → (𝑢 “ (𝑣𝐾)) ⊆ (𝑢 ran 𝑘))
211209, 210syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 “ (𝑣𝐾)) ⊆ (𝑢 ran 𝑘))
212 simprlr 779 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 ran 𝑘) ⊆ 𝑉)
213211, 212sstrd 3925 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 “ (𝑣𝐾)) ⊆ 𝑉)
214199, 213eqsstrid 3963 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → ((𝑢𝑣) “ 𝐾) ⊆ 𝑉)
215196, 198, 214elrabd 3630 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
216194, 215eqeltrd 2890 . . . . . . . . . . . 12 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
217184, 216sylan2b 596 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) → (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
218217ralrimivva 3156 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
219189mpofun 7255 . . . . . . . . . . 11 Fun 𝐹
220 ssrab2 4007 . . . . . . . . . . . . 13 {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
221 ssrab2 4007 . . . . . . . . . . . . 13 {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ⊆ (𝑅 Cn 𝑆)
222 xpss12 5534 . . . . . . . . . . . . 13 (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
223220, 221, 222mp2an 691 . . . . . . . . . . . 12 ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
224 vex 3444 . . . . . . . . . . . . . 14 𝑓 ∈ V
225 vex 3444 . . . . . . . . . . . . . 14 𝑔 ∈ V
226224, 225coex 7619 . . . . . . . . . . . . 13 (𝑓𝑔) ∈ V
227189, 226dmmpo 7753 . . . . . . . . . . . 12 dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
228223, 227sseqtrri 3952 . . . . . . . . . . 11 ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹
229 funimassov 7306 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
230219, 228, 229mp2an 691 . . . . . . . . . 10 ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
231218, 230sylibr 237 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
232 funimass3 6801 . . . . . . . . . 10 ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
233219, 228, 232mp2an 691 . . . . . . . . 9 ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
234231, 233sylib 221 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
235 eleq2 2878 . . . . . . . . . 10 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})))
236 sseq1 3940 . . . . . . . . . 10 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → (𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
237235, 236anbi12d 633 . . . . . . . . 9 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
238237rspcev 3571 . . . . . . . 8 ((({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅)) ∧ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
239136, 177, 234, 238syl12anc 835 . . . . . . 7 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
240239expr 460 . . . . . 6 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝐵𝐾) = 𝑤) → ((𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
241240exlimdv 1934 . . . . 5 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝐵𝐾) = 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
24288, 241syldan 594 . . . 4 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝑆t (𝐵𝐾)) = 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
243242expimpd 457 . . 3 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → (( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
244243rexlimdva 3243 . 2 (𝜑 → (∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
24585, 244mpd 15 1 (𝜑 → ∃𝑧 ∈ ((𝑇ko 𝑆) ×t (𝑆ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497  ⟨cop 4531  ∪ cuni 4800  ∪ ciun 4881   × cxp 5517  ◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522   ∘ ccom 5523  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137  Fincfn 8494   ↾t crest 16688  Topctop 21505  intcnt 21629   Cn ccn 21836  Compccmp 21998  𝑛-Locally cnlly 22077   ×t ctx 22172   ↑ko cxko 22173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-fin 8498  df-fi 8861  df-rest 16690  df-topgen 16711  df-top 21506  df-topon 21523  df-bases 21558  df-ntr 21632  df-nei 21710  df-cn 21839  df-cmp 21999  df-nlly 22079  df-tx 22174  df-xko 22175 This theorem is referenced by:  xkococn  22272
 Copyright terms: Public domain W3C validator