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

Theorem xkococnlem 21510
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 21248 . . . 4 ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅t 𝐾) ∈ Comp) → (𝑆t (𝐵𝐾)) ∈ Comp)
41, 2, 3syl2anc 694 . . 3 (𝜑 → (𝑆t (𝐵𝐾)) ∈ Comp)
5 xkococn.s . . . . . . . . 9 (𝜑𝑆 ∈ 𝑛-Locally Comp)
65adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → 𝑆 ∈ 𝑛-Locally Comp)
7 xkococn.a . . . . . . . . . 10 (𝜑𝐴 ∈ (𝑆 Cn 𝑇))
8 xkococn.v . . . . . . . . . 10 (𝜑𝑉𝑇)
9 cnima 21117 . . . . . . . . . 10 ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉𝑇) → (𝐴𝑉) ∈ 𝑆)
107, 8, 9syl2anc 694 . . . . . . . . 9 (𝜑 → (𝐴𝑉) ∈ 𝑆)
1110adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → (𝐴𝑉) ∈ 𝑆)
12 imaco 5678 . . . . . . . . . . 11 ((𝐴𝐵) “ 𝐾) = (𝐴 “ (𝐵𝐾))
13 xkococn.i . . . . . . . . . . 11 (𝜑 → ((𝐴𝐵) “ 𝐾) ⊆ 𝑉)
1412, 13syl5eqssr 3683 . . . . . . . . . 10 (𝜑 → (𝐴 “ (𝐵𝐾)) ⊆ 𝑉)
15 eqid 2651 . . . . . . . . . . . . 13 𝑆 = 𝑆
16 eqid 2651 . . . . . . . . . . . . 13 𝑇 = 𝑇
1715, 16cnf 21098 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴: 𝑆 𝑇)
18 ffun 6086 . . . . . . . . . . . 12 (𝐴: 𝑆 𝑇 → Fun 𝐴)
197, 17, 183syl 18 . . . . . . . . . . 11 (𝜑 → Fun 𝐴)
20 imassrn 5512 . . . . . . . . . . . . 13 (𝐵𝐾) ⊆ ran 𝐵
21 eqid 2651 . . . . . . . . . . . . . . 15 𝑅 = 𝑅
2221, 15cnf 21098 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵: 𝑅 𝑆)
23 frn 6091 . . . . . . . . . . . . . 14 (𝐵: 𝑅 𝑆 → ran 𝐵 𝑆)
241, 22, 233syl 18 . . . . . . . . . . . . 13 (𝜑 → ran 𝐵 𝑆)
2520, 24syl5ss 3647 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐾) ⊆ 𝑆)
26 fdm 6089 . . . . . . . . . . . . 13 (𝐴: 𝑆 𝑇 → dom 𝐴 = 𝑆)
277, 17, 263syl 18 . . . . . . . . . . . 12 (𝜑 → dom 𝐴 = 𝑆)
2825, 27sseqtr4d 3675 . . . . . . . . . . 11 (𝜑 → (𝐵𝐾) ⊆ dom 𝐴)
29 funimass3 6373 . . . . . . . . . . 11 ((Fun 𝐴 ∧ (𝐵𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵𝐾)) ⊆ 𝑉 ↔ (𝐵𝐾) ⊆ (𝐴𝑉)))
3019, 28, 29syl2anc 694 . . . . . . . . . 10 (𝜑 → ((𝐴 “ (𝐵𝐾)) ⊆ 𝑉 ↔ (𝐵𝐾) ⊆ (𝐴𝑉)))
3114, 30mpbid 222 . . . . . . . . 9 (𝜑 → (𝐵𝐾) ⊆ (𝐴𝑉))
3231sselda 3636 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → 𝑥 ∈ (𝐴𝑉))
33 nlly2i 21327 . . . . . . . 8 ((𝑆 ∈ 𝑛-Locally Comp ∧ (𝐴𝑉) ∈ 𝑆𝑥 ∈ (𝐴𝑉)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))
346, 11, 32, 33syl3anc 1366 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))
35 nllytop 21324 . . . . . . . . . . . . 13 (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
365, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Top)
3736ad3antrrr 766 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38 imaexg 7145 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵𝐾) ∈ V)
391, 38syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐾) ∈ V)
4039ad3antrrr 766 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝐵𝐾) ∈ V)
41 simprl 809 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢𝑆)
42 elrestr 16136 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ (𝐵𝐾) ∈ V ∧ 𝑢𝑆) → (𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)))
4337, 40, 41, 42syl3anc 1366 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)))
44 simprr1 1129 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥𝑢)
45 simpllr 815 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵𝐾))
4644, 45elind 3831 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵𝐾)))
47 inss1 3866 . . . . . . . . . . . 12 (𝑢 ∩ (𝐵𝐾)) ⊆ 𝑢
48 elpwi 4201 . . . . . . . . . . . . . . 15 (𝑠 ∈ 𝒫 (𝐴𝑉) → 𝑠 ⊆ (𝐴𝑉))
4948ad2antlr 763 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑠 ⊆ (𝐴𝑉))
50 elssuni 4499 . . . . . . . . . . . . . . . 16 ((𝐴𝑉) ∈ 𝑆 → (𝐴𝑉) ⊆ 𝑆)
5110, 50syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝑉) ⊆ 𝑆)
5251ad3antrrr 766 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝐴𝑉) ⊆ 𝑆)
5349, 52sstrd 3646 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑠 𝑆)
54 simprr2 1130 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢𝑠)
5515ssntr 20910 . . . . . . . . . . . . 13 (((𝑆 ∈ Top ∧ 𝑠 𝑆) ∧ (𝑢𝑆𝑢𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
5637, 53, 41, 54, 55syl22anc 1367 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
5747, 56syl5ss 3647 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58 simprr3 1131 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑆t 𝑠) ∈ Comp)
5957, 58jca 553 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))
60 eleq2 2719 . . . . . . . . . . . 12 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → (𝑥𝑦𝑥 ∈ (𝑢 ∩ (𝐵𝐾))))
61 sseq1 3659 . . . . . . . . . . . . 13 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ (𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠)))
6261anbi1d 741 . . . . . . . . . . . 12 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6360, 62anbi12d 747 . . . . . . . . . . 11 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → ((𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵𝐾)) ∧ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6463rspcev 3340 . . . . . . . . . 10 (((𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵𝐾)) ∧ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6543, 46, 59, 64syl12anc 1364 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6665rexlimdvaa 3061 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) → (∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6766reximdva 3046 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵𝐾)) → (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6834, 67mpd 15 . . . . . 6 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
69 rexcom 3128 . . . . . . 7 (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
70 r19.42v 3121 . . . . . . . 8 (∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ (𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7170rexbii 3070 . . . . . . 7 (∃𝑦 ∈ (𝑆t (𝐵𝐾))∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7269, 71bitri 264 . . . . . 6 (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7368, 72sylib 208 . . . . 5 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7473ralrimiva 2995 . . . 4 (𝜑 → ∀𝑥 ∈ (𝐵𝐾)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7515restuni 21014 . . . . . 6 ((𝑆 ∈ Top ∧ (𝐵𝐾) ⊆ 𝑆) → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
7636, 25, 75syl2anc 694 . . . . 5 (𝜑 → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
7776raleqdv 3174 . . . 4 (𝜑 → (∀𝑥 ∈ (𝐵𝐾)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
7874, 77mpbid 222 . . 3 (𝜑 → ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
79 eqid 2651 . . . 4 (𝑆t (𝐵𝐾)) = (𝑆t (𝐵𝐾))
80 fveq2 6229 . . . . . 6 (𝑠 = (𝑘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘𝑦)))
8180sseq2d 3666 . . . . 5 (𝑠 = (𝑘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦))))
82 oveq2 6698 . . . . . 6 (𝑠 = (𝑘𝑦) → (𝑆t 𝑠) = (𝑆t (𝑘𝑦)))
8382eleq1d 2715 . . . . 5 (𝑠 = (𝑘𝑦) → ((𝑆t 𝑠) ∈ Comp ↔ (𝑆t (𝑘𝑦)) ∈ Comp))
8481, 83anbi12d 747 . . . 4 (𝑠 = (𝑘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))
8579, 84cmpcovf 21242 . . 3 (((𝑆t (𝐵𝐾)) ∈ Comp ∧ ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))))
864, 78, 85syl2anc 694 . 2 (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))))
8776adantr 480 . . . . . . 7 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
8887eqeq1d 2653 . . . . . 6 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → ((𝐵𝐾) = 𝑤 (𝑆t (𝐵𝐾)) = 𝑤))
8988biimpar 501 . . . . 5 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝑆t (𝐵𝐾)) = 𝑤) → (𝐵𝐾) = 𝑤)
9036ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
91 cntop2 21093 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
927, 91syl 17 . . . . . . . . . . 11 (𝜑𝑇 ∈ Top)
9392ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
94 xkotop 21439 . . . . . . . . . 10 ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ^ko 𝑆) ∈ Top)
9590, 93, 94syl2anc 694 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑇 ^ko 𝑆) ∈ Top)
96 cntop1 21092 . . . . . . . . . . . 12 (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
971, 96syl 17 . . . . . . . . . . 11 (𝜑𝑅 ∈ Top)
9897ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
99 xkotop 21439 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ Top)
10098, 90, 99syl2anc 694 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆 ^ko 𝑅) ∈ Top)
101 simprrl 821 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (𝐴𝑉))
102 frn 6091 . . . . . . . . . . . . 13 (𝑘:𝑤⟶𝒫 (𝐴𝑉) → ran 𝑘 ⊆ 𝒫 (𝐴𝑉))
103101, 102syl 17 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (𝐴𝑉))
104 sspwuni 4643 . . . . . . . . . . . 12 (ran 𝑘 ⊆ 𝒫 (𝐴𝑉) ↔ ran 𝑘 ⊆ (𝐴𝑉))
105103, 104sylib 208 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ (𝐴𝑉))
10610ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴𝑉) ∈ 𝑆)
107106, 50syl 17 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴𝑉) ⊆ 𝑆)
108105, 107sstrd 3646 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 𝑆)
109 ffn 6083 . . . . . . . . . . . . 13 (𝑘:𝑤⟶𝒫 (𝐴𝑉) → 𝑘 Fn 𝑤)
110 fniunfv 6545 . . . . . . . . . . . . 13 (𝑘 Fn 𝑤 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
111101, 109, 1103syl 18 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
112111oveq2d 6706 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t 𝑦𝑤 (𝑘𝑦)) = (𝑆t ran 𝑘))
113 inss2 3867 . . . . . . . . . . . . 13 (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin) ⊆ Fin
114 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin))
115113, 114sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
116 simprrr 822 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))
117 simpr 476 . . . . . . . . . . . . . 14 ((𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → (𝑆t (𝑘𝑦)) ∈ Comp)
118117ralimi 2981 . . . . . . . . . . . . 13 (∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp)
119116, 118syl 17 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp)
12015fiuncmp 21255 . . . . . . . . . . . 12 ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp) → (𝑆t 𝑦𝑤 (𝑘𝑦)) ∈ Comp)
12190, 115, 119, 120syl3anc 1366 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t 𝑦𝑤 (𝑘𝑦)) ∈ Comp)
122112, 121eqeltrrd 2731 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t ran 𝑘) ∈ Comp)
1238ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑉𝑇)
12415, 90, 93, 108, 122, 123xkoopn 21440 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ^ko 𝑆))
125 xkococn.k . . . . . . . . . . 11 (𝜑𝐾 𝑅)
126125ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐾 𝑅)
1272ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑅t 𝐾) ∈ Comp)
128111, 108eqsstrd 3672 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
129 iunss 4593 . . . . . . . . . . . . 13 ( 𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
130128, 129sylib 208 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
13115ntropn 20901 . . . . . . . . . . . . . 14 ((𝑆 ∈ Top ∧ (𝑘𝑦) ⊆ 𝑆) → ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
132131ex 449 . . . . . . . . . . . . 13 (𝑆 ∈ Top → ((𝑘𝑦) ⊆ 𝑆 → ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆))
133132ralimdv 2992 . . . . . . . . . . . 12 (𝑆 ∈ Top → (∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆))
13490, 130, 133sylc 65 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
135 iunopn 20751 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
13690, 134, 135syl2anc 694 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
13721, 98, 90, 126, 127, 136xkoopn 21440 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ∈ (𝑆 ^ko 𝑅))
138 txopn 21453 . . . . . . . . 9 ((((𝑇 ^ko 𝑆) ∈ Top ∧ (𝑆 ^ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ^ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ∈ (𝑆 ^ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅)))
13995, 100, 124, 137, 138syl22anc 1367 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅)))
1407ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
141 imaiun 6543 . . . . . . . . . . . 12 (𝐴 𝑦𝑤 (𝑘𝑦)) = 𝑦𝑤 (𝐴 “ (𝑘𝑦))
142111imaeq2d 5501 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴 𝑦𝑤 (𝑘𝑦)) = (𝐴 ran 𝑘))
143141, 142syl5eqr 2699 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝐴 “ (𝑘𝑦)) = (𝐴 ran 𝑘))
144111, 105eqsstrd 3672 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉))
14519ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → Fun 𝐴)
146101, 109syl 17 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
14727ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → dom 𝐴 = 𝑆)
148108, 147sseqtr4d 3675 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ dom 𝐴)
149 simpl1 1084 . . . . . . . . . . . . . . . 16 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → Fun 𝐴)
1501103ad2ant2 1103 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
151 simp3 1083 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ran 𝑘 ⊆ dom 𝐴)
152150, 151eqsstrd 3672 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → 𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
153 iunss 4593 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
154152, 153sylib 208 . . . . . . . . . . . . . . . . 17 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ∀𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
155154r19.21bi 2961 . . . . . . . . . . . . . . . 16 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → (𝑘𝑦) ⊆ dom 𝐴)
156 funimass3 6373 . . . . . . . . . . . . . . . 16 ((Fun 𝐴 ∧ (𝑘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ (𝑘𝑦) ⊆ (𝐴𝑉)))
157149, 155, 156syl2anc 694 . . . . . . . . . . . . . . 15 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → ((𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ (𝑘𝑦) ⊆ (𝐴𝑉)))
158157ralbidva 3014 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → (∀𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
159 iunss 4593 . . . . . . . . . . . . . 14 ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ ∀𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉)
160 iunss 4593 . . . . . . . . . . . . . 14 ( 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉) ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉))
161158, 159, 1603bitr4g 303 . . . . . . . . . . . . 13 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
162145, 146, 148, 161syl3anc 1366 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
163144, 162mpbird 247 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉)
164143, 163eqsstr3d 3673 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴 ran 𝑘) ⊆ 𝑉)
165 imaeq1 5496 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (𝑎 ran 𝑘) = (𝐴 ran 𝑘))
166165sseq1d 3665 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((𝑎 ran 𝑘) ⊆ 𝑉 ↔ (𝐴 ran 𝑘) ⊆ 𝑉))
167166elrab 3396 . . . . . . . . . 10 (𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ↔ (𝐴 ∈ (𝑆 Cn 𝑇) ∧ (𝐴 ran 𝑘) ⊆ 𝑉))
168140, 164, 167sylanbrc 699 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉})
1691ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
170 simprl 809 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) = 𝑤)
171 uniiun 4605 . . . . . . . . . . . 12 𝑤 = 𝑦𝑤 𝑦
172170, 171syl6eq 2701 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) = 𝑦𝑤 𝑦)
173 simpl 472 . . . . . . . . . . . . 13 ((𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)))
174173ralimi 2981 . . . . . . . . . . . 12 (∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → ∀𝑦𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)))
175 ss2iun 4568 . . . . . . . . . . . 12 (∀𝑦𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) → 𝑦𝑤 𝑦 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
176116, 174, 1753syl 18 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 𝑦 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
177172, 176eqsstrd 3672 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
178 imaeq1 5496 . . . . . . . . . . . 12 (𝑏 = 𝐵 → (𝑏𝐾) = (𝐵𝐾))
179178sseq1d 3665 . . . . . . . . . . 11 (𝑏 = 𝐵 → ((𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ↔ (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
180179elrab 3396 . . . . . . . . . 10 (𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ↔ (𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
181169, 177, 180sylanbrc 699 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})
182 opelxpi 5182 . . . . . . . . 9 ((𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}))
183168, 181, 182syl2anc 694 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}))
184 imaeq1 5496 . . . . . . . . . . . . . . 15 (𝑎 = 𝑢 → (𝑎 ran 𝑘) = (𝑢 ran 𝑘))
185184sseq1d 3665 . . . . . . . . . . . . . 14 (𝑎 = 𝑢 → ((𝑎 ran 𝑘) ⊆ 𝑉 ↔ (𝑢 ran 𝑘) ⊆ 𝑉))
186185elrab 3396 . . . . . . . . . . . . 13 (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉))
187 imaeq1 5496 . . . . . . . . . . . . . . 15 (𝑏 = 𝑣 → (𝑏𝐾) = (𝑣𝐾))
188187sseq1d 3665 . . . . . . . . . . . . . 14 (𝑏 = 𝑣 → ((𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ↔ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
189188elrab 3396 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
190186, 189anbi12i 733 . . . . . . . . . . . 12 ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))))
191 simprll 819 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
192 simprrl 821 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
193 coeq1 5312 . . . . . . . . . . . . . . 15 (𝑓 = 𝑢 → (𝑓𝑔) = (𝑢𝑔))
194 coeq2 5313 . . . . . . . . . . . . . . 15 (𝑔 = 𝑣 → (𝑢𝑔) = (𝑢𝑣))
195 xkococn.1 . . . . . . . . . . . . . . 15 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓𝑔))
196 vex 3234 . . . . . . . . . . . . . . . 16 𝑢 ∈ V
197 vex 3234 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
198196, 197coex 7160 . . . . . . . . . . . . . . 15 (𝑢𝑣) ∈ V
199193, 194, 195, 198ovmpt2 6838 . . . . . . . . . . . . . 14 ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢𝑣))
200191, 192, 199syl2anc 694 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝐹𝑣) = (𝑢𝑣))
201 cnco 21118 . . . . . . . . . . . . . . 15 ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢𝑣) ∈ (𝑅 Cn 𝑇))
202192, 191, 201syl2anc 694 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝑣) ∈ (𝑅 Cn 𝑇))
203 imaco 5678 . . . . . . . . . . . . . . 15 ((𝑢𝑣) “ 𝐾) = (𝑢 “ (𝑣𝐾))
204 simprrr 822 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
20515ntrss2 20909 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ Top ∧ (𝑘𝑦) ⊆ 𝑆) → ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦))
206205ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ Top → ((𝑘𝑦) ⊆ 𝑆 → ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦)))
207206ralimdv 2992 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ Top → (∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦)))
20890, 130, 207sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦))
209 ss2iun 4568 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ 𝑦𝑤 (𝑘𝑦))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ 𝑦𝑤 (𝑘𝑦))
211210, 111sseqtrd 3674 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ ran 𝑘)
212211adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ ran 𝑘)
213204, 212sstrd 3646 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑣𝐾) ⊆ ran 𝑘)
214 imass2 5536 . . . . . . . . . . . . . . . . 17 ((𝑣𝐾) ⊆ ran 𝑘 → (𝑢 “ (𝑣𝐾)) ⊆ (𝑢 ran 𝑘))
215213, 214syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 “ (𝑣𝐾)) ⊆ (𝑢 ran 𝑘))
216 simprlr 820 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 ran 𝑘) ⊆ 𝑉)
217215, 216sstrd 3646 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 “ (𝑣𝐾)) ⊆ 𝑉)
218203, 217syl5eqss 3682 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → ((𝑢𝑣) “ 𝐾) ⊆ 𝑉)
219 imaeq1 5496 . . . . . . . . . . . . . . . 16 ( = (𝑢𝑣) → (𝐾) = ((𝑢𝑣) “ 𝐾))
220219sseq1d 3665 . . . . . . . . . . . . . . 15 ( = (𝑢𝑣) → ((𝐾) ⊆ 𝑉 ↔ ((𝑢𝑣) “ 𝐾) ⊆ 𝑉))
221220elrab 3396 . . . . . . . . . . . . . 14 ((𝑢𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ((𝑢𝑣) ∈ (𝑅 Cn 𝑇) ∧ ((𝑢𝑣) “ 𝐾) ⊆ 𝑉))
222202, 218, 221sylanbrc 699 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
223200, 222eqeltrd 2730 . . . . . . . . . . . 12 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
224190, 223sylan2b 491 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) → (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
225224ralrimivva 3000 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
226195mpt2fun 6804 . . . . . . . . . . 11 Fun 𝐹
227 ssrab2 3720 . . . . . . . . . . . . 13 {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
228 ssrab2 3720 . . . . . . . . . . . . 13 {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ⊆ (𝑅 Cn 𝑆)
229 xpss12 5158 . . . . . . . . . . . . 13 (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
230227, 228, 229mp2an 708 . . . . . . . . . . . 12 ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
231 vex 3234 . . . . . . . . . . . . . 14 𝑓 ∈ V
232 vex 3234 . . . . . . . . . . . . . 14 𝑔 ∈ V
233231, 232coex 7160 . . . . . . . . . . . . 13 (𝑓𝑔) ∈ V
234195, 233dmmpt2 7285 . . . . . . . . . . . 12 dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
235230, 234sseqtr4i 3671 . . . . . . . . . . 11 ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹
236 funimassov 6853 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
237226, 235, 236mp2an 708 . . . . . . . . . 10 ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
238225, 237sylibr 224 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
239 funimass3 6373 . . . . . . . . . 10 ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
240226, 235, 239mp2an 708 . . . . . . . . 9 ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
241238, 240sylib 208 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
242 eleq2 2719 . . . . . . . . . 10 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})))
243 sseq1 3659 . . . . . . . . . 10 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → (𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
244242, 243anbi12d 747 . . . . . . . . 9 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
245244rspcev 3340 . . . . . . . 8 ((({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅)) ∧ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
246139, 183, 241, 245syl12anc 1364 . . . . . . 7 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
247246expr 642 . . . . . 6 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝐵𝐾) = 𝑤) → ((𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
248247exlimdv 1901 . . . . 5 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝐵𝐾) = 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
24989, 248syldan 486 . . . 4 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝑆t (𝐵𝐾)) = 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
250249expimpd 628 . . 3 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → (( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
251250rexlimdva 3060 . 2 (𝜑 → (∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
25286, 251mpd 15 1 (𝜑 → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cin 3606  wss 3607  𝒫 cpw 4191  cop 4216   cuni 4468   ciun 4552   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cima 5146  ccom 5147  Fun wfun 5920   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  Fincfn 7997  t crest 16128  Topctop 20746  intcnt 20869   Cn ccn 21076  Compccmp 21237  𝑛-Locally cnlly 21316   ×t ctx 21411   ^ko cxko 21412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-fin 8001  df-fi 8358  df-rest 16130  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-ntr 20872  df-nei 20950  df-cn 21079  df-cmp 21238  df-nlly 21318  df-tx 21413  df-xko 21414
This theorem is referenced by:  xkococn  21511
  Copyright terms: Public domain W3C validator