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

Theorem xkococnlem 21372
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 21110 . . . 4 ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅t 𝐾) ∈ Comp) → (𝑆t (𝐵𝐾)) ∈ Comp)
41, 2, 3syl2anc 692 . . 3 (𝜑 → (𝑆t (𝐵𝐾)) ∈ Comp)
5 xkococn.s . . . . . . . . 9 (𝜑𝑆 ∈ 𝑛-Locally Comp)
65adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → 𝑆 ∈ 𝑛-Locally Comp)
7 xkococn.a . . . . . . . . . 10 (𝜑𝐴 ∈ (𝑆 Cn 𝑇))
8 xkococn.v . . . . . . . . . 10 (𝜑𝑉𝑇)
9 cnima 20979 . . . . . . . . . 10 ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉𝑇) → (𝐴𝑉) ∈ 𝑆)
107, 8, 9syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐴𝑉) ∈ 𝑆)
1110adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → (𝐴𝑉) ∈ 𝑆)
12 imaco 5599 . . . . . . . . . . 11 ((𝐴𝐵) “ 𝐾) = (𝐴 “ (𝐵𝐾))
13 xkococn.i . . . . . . . . . . 11 (𝜑 → ((𝐴𝐵) “ 𝐾) ⊆ 𝑉)
1412, 13syl5eqssr 3629 . . . . . . . . . 10 (𝜑 → (𝐴 “ (𝐵𝐾)) ⊆ 𝑉)
15 eqid 2621 . . . . . . . . . . . . 13 𝑆 = 𝑆
16 eqid 2621 . . . . . . . . . . . . 13 𝑇 = 𝑇
1715, 16cnf 20960 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴: 𝑆 𝑇)
18 ffun 6005 . . . . . . . . . . . 12 (𝐴: 𝑆 𝑇 → Fun 𝐴)
197, 17, 183syl 18 . . . . . . . . . . 11 (𝜑 → Fun 𝐴)
20 imassrn 5436 . . . . . . . . . . . . 13 (𝐵𝐾) ⊆ ran 𝐵
21 eqid 2621 . . . . . . . . . . . . . . 15 𝑅 = 𝑅
2221, 15cnf 20960 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵: 𝑅 𝑆)
23 frn 6010 . . . . . . . . . . . . . 14 (𝐵: 𝑅 𝑆 → ran 𝐵 𝑆)
241, 22, 233syl 18 . . . . . . . . . . . . 13 (𝜑 → ran 𝐵 𝑆)
2520, 24syl5ss 3594 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐾) ⊆ 𝑆)
26 fdm 6008 . . . . . . . . . . . . 13 (𝐴: 𝑆 𝑇 → dom 𝐴 = 𝑆)
277, 17, 263syl 18 . . . . . . . . . . . 12 (𝜑 → dom 𝐴 = 𝑆)
2825, 27sseqtr4d 3621 . . . . . . . . . . 11 (𝜑 → (𝐵𝐾) ⊆ dom 𝐴)
29 funimass3 6289 . . . . . . . . . . 11 ((Fun 𝐴 ∧ (𝐵𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵𝐾)) ⊆ 𝑉 ↔ (𝐵𝐾) ⊆ (𝐴𝑉)))
3019, 28, 29syl2anc 692 . . . . . . . . . 10 (𝜑 → ((𝐴 “ (𝐵𝐾)) ⊆ 𝑉 ↔ (𝐵𝐾) ⊆ (𝐴𝑉)))
3114, 30mpbid 222 . . . . . . . . 9 (𝜑 → (𝐵𝐾) ⊆ (𝐴𝑉))
3231sselda 3583 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵𝐾)) → 𝑥 ∈ (𝐴𝑉))
33 nlly2i 21189 . . . . . . . 8 ((𝑆 ∈ 𝑛-Locally Comp ∧ (𝐴𝑉) ∈ 𝑆𝑥 ∈ (𝐴𝑉)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))
346, 11, 32, 33syl3anc 1323 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))
35 nllytop 21186 . . . . . . . . . . . . 13 (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
365, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Top)
3736ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38 imaexg 7050 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵𝐾) ∈ V)
391, 38syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐾) ∈ V)
4039ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝐵𝐾) ∈ V)
41 simprl 793 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢𝑆)
42 elrestr 16010 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ (𝐵𝐾) ∈ V ∧ 𝑢𝑆) → (𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)))
4337, 40, 41, 42syl3anc 1323 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)))
44 simprr1 1107 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥𝑢)
45 simpllr 798 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵𝐾))
4644, 45elind 3776 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵𝐾)))
47 inss1 3811 . . . . . . . . . . . 12 (𝑢 ∩ (𝐵𝐾)) ⊆ 𝑢
48 elpwi 4140 . . . . . . . . . . . . . . 15 (𝑠 ∈ 𝒫 (𝐴𝑉) → 𝑠 ⊆ (𝐴𝑉))
4948ad2antlr 762 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑠 ⊆ (𝐴𝑉))
50 elssuni 4433 . . . . . . . . . . . . . . . 16 ((𝐴𝑉) ∈ 𝑆 → (𝐴𝑉) ⊆ 𝑆)
5110, 50syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝑉) ⊆ 𝑆)
5251ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝐴𝑉) ⊆ 𝑆)
5349, 52sstrd 3593 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑠 𝑆)
54 simprr2 1108 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢𝑠)
5515ssntr 20772 . . . . . . . . . . . . 13 (((𝑆 ∈ Top ∧ 𝑠 𝑆) ∧ (𝑢𝑆𝑢𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
5637, 53, 41, 54, 55syl22anc 1324 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
5747, 56syl5ss 3594 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58 simprr3 1109 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → (𝑆t 𝑠) ∈ Comp)
5957, 58jca 554 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))
60 eleq2 2687 . . . . . . . . . . . 12 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → (𝑥𝑦𝑥 ∈ (𝑢 ∩ (𝐵𝐾))))
61 sseq1 3605 . . . . . . . . . . . . 13 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ (𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠)))
6261anbi1d 740 . . . . . . . . . . . 12 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6360, 62anbi12d 746 . . . . . . . . . . 11 (𝑦 = (𝑢 ∩ (𝐵𝐾)) → ((𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵𝐾)) ∧ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6463rspcev 3295 . . . . . . . . . 10 (((𝑢 ∩ (𝐵𝐾)) ∈ (𝑆t (𝐵𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵𝐾)) ∧ ((𝑢 ∩ (𝐵𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6543, 46, 59, 64syl12anc 1321 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) ∧ (𝑢𝑆 ∧ (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
6665rexlimdvaa 3025 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐵𝐾)) ∧ 𝑠 ∈ 𝒫 (𝐴𝑉)) → (∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6766reximdva 3011 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵𝐾)) → (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑢𝑆 (𝑥𝑢𝑢𝑠 ∧ (𝑆t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
6834, 67mpd 15 . . . . . 6 ((𝜑𝑥 ∈ (𝐵𝐾)) → ∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
69 rexcom 3091 . . . . . . 7 (∃𝑠 ∈ 𝒫 (𝐴𝑉)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆t (𝐵𝐾))∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
70 r19.42v 3084 . . . . . . . 8 (∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑥𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ (𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7170rexbii 3034 . . . . . . 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 2960 . . . 4 (𝜑 → ∀𝑥 ∈ (𝐵𝐾)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
7515restuni 20876 . . . . . 6 ((𝑆 ∈ Top ∧ (𝐵𝐾) ⊆ 𝑆) → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
7636, 25, 75syl2anc 692 . . . . 5 (𝜑 → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
7776raleqdv 3133 . . . 4 (𝜑 → (∀𝑥 ∈ (𝐵𝐾)∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)) ↔ ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))))
7874, 77mpbid 222 . . 3 (𝜑 → ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp)))
79 eqid 2621 . . . 4 (𝑆t (𝐵𝐾)) = (𝑆t (𝐵𝐾))
80 fveq2 6148 . . . . . 6 (𝑠 = (𝑘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘𝑦)))
8180sseq2d 3612 . . . . 5 (𝑠 = (𝑘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦))))
82 oveq2 6612 . . . . . 6 (𝑠 = (𝑘𝑦) → (𝑆t 𝑠) = (𝑆t (𝑘𝑦)))
8382eleq1d 2683 . . . . 5 (𝑠 = (𝑘𝑦) → ((𝑆t 𝑠) ∈ Comp ↔ (𝑆t (𝑘𝑦)) ∈ Comp))
8481, 83anbi12d 746 . . . 4 (𝑠 = (𝑘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))
8579, 84cmpcovf 21104 . . 3 (((𝑆t (𝐵𝐾)) ∈ Comp ∧ ∀𝑥 (𝑆t (𝐵𝐾))∃𝑦 ∈ (𝑆t (𝐵𝐾))(𝑥𝑦 ∧ ∃𝑠 ∈ 𝒫 (𝐴𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))))
864, 78, 85syl2anc 692 . 2 (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)( (𝑆t (𝐵𝐾)) = 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))))
8776adantr 481 . . . . . . 7 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → (𝐵𝐾) = (𝑆t (𝐵𝐾)))
8887eqeq1d 2623 . . . . . 6 ((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) → ((𝐵𝐾) = 𝑤 (𝑆t (𝐵𝐾)) = 𝑤))
8988biimpar 502 . . . . 5 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝑆t (𝐵𝐾)) = 𝑤) → (𝐵𝐾) = 𝑤)
9036ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
91 cntop2 20955 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
927, 91syl 17 . . . . . . . . . . 11 (𝜑𝑇 ∈ Top)
9392ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
94 xkotop 21301 . . . . . . . . . 10 ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ^ko 𝑆) ∈ Top)
9590, 93, 94syl2anc 692 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑇 ^ko 𝑆) ∈ Top)
96 cntop1 20954 . . . . . . . . . . . 12 (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
971, 96syl 17 . . . . . . . . . . 11 (𝜑𝑅 ∈ Top)
9897ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
99 xkotop 21301 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ Top)
10098, 90, 99syl2anc 692 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆 ^ko 𝑅) ∈ Top)
101 simprrl 803 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (𝐴𝑉))
102 frn 6010 . . . . . . . . . . . . 13 (𝑘:𝑤⟶𝒫 (𝐴𝑉) → ran 𝑘 ⊆ 𝒫 (𝐴𝑉))
103101, 102syl 17 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (𝐴𝑉))
104 sspwuni 4577 . . . . . . . . . . . 12 (ran 𝑘 ⊆ 𝒫 (𝐴𝑉) ↔ ran 𝑘 ⊆ (𝐴𝑉))
105103, 104sylib 208 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ (𝐴𝑉))
10610ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴𝑉) ∈ 𝑆)
107106, 50syl 17 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴𝑉) ⊆ 𝑆)
108105, 107sstrd 3593 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 𝑆)
109 ffn 6002 . . . . . . . . . . . . 13 (𝑘:𝑤⟶𝒫 (𝐴𝑉) → 𝑘 Fn 𝑤)
110 fniunfv 6459 . . . . . . . . . . . . 13 (𝑘 Fn 𝑤 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
111101, 109, 1103syl 18 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
112111oveq2d 6620 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t 𝑦𝑤 (𝑘𝑦)) = (𝑆t ran 𝑘))
113 inss2 3812 . . . . . . . . . . . . 13 (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin) ⊆ Fin
114 simplr 791 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin))
115113, 114sseldi 3581 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
116 simprrr 804 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp))
117 simpr 477 . . . . . . . . . . . . . 14 ((𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → (𝑆t (𝑘𝑦)) ∈ Comp)
118117ralimi 2947 . . . . . . . . . . . . 13 (∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp)
119116, 118syl 17 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp)
12015fiuncmp 21117 . . . . . . . . . . . 12 ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦𝑤 (𝑆t (𝑘𝑦)) ∈ Comp) → (𝑆t 𝑦𝑤 (𝑘𝑦)) ∈ Comp)
12190, 115, 119, 120syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t 𝑦𝑤 (𝑘𝑦)) ∈ Comp)
122112, 121eqeltrrd 2699 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑆t ran 𝑘) ∈ Comp)
1238ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑉𝑇)
12415, 90, 93, 108, 122, 123xkoopn 21302 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ^ko 𝑆))
125 xkococn.k . . . . . . . . . . 11 (𝜑𝐾 𝑅)
126125ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐾 𝑅)
1272ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝑅t 𝐾) ∈ Comp)
128111, 108eqsstrd 3618 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
129 iunss 4527 . . . . . . . . . . . . 13 ( 𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
130128, 129sylib 208 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆)
13115ntropn 20763 . . . . . . . . . . . . . 14 ((𝑆 ∈ Top ∧ (𝑘𝑦) ⊆ 𝑆) → ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
132131ex 450 . . . . . . . . . . . . 13 (𝑆 ∈ Top → ((𝑘𝑦) ⊆ 𝑆 → ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆))
133132ralimdv 2957 . . . . . . . . . . . 12 (𝑆 ∈ Top → (∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆))
13490, 130, 133sylc 65 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
135 iunopn 20628 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
13690, 134, 135syl2anc 692 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ∈ 𝑆)
13721, 98, 90, 126, 127, 136xkoopn 21302 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ∈ (𝑆 ^ko 𝑅))
138 txopn 21315 . . . . . . . . 9 ((((𝑇 ^ko 𝑆) ∈ Top ∧ (𝑆 ^ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ^ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ∈ (𝑆 ^ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅)))
13995, 100, 124, 137, 138syl22anc 1324 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅)))
1407ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
141 imaiun 6457 . . . . . . . . . . . 12 (𝐴 𝑦𝑤 (𝑘𝑦)) = 𝑦𝑤 (𝐴 “ (𝑘𝑦))
142111imaeq2d 5425 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴 𝑦𝑤 (𝑘𝑦)) = (𝐴 ran 𝑘))
143141, 142syl5eqr 2669 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝐴 “ (𝑘𝑦)) = (𝐴 ran 𝑘))
144111, 105eqsstrd 3618 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉))
14519ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → Fun 𝐴)
146101, 109syl 17 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
14727ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → dom 𝐴 = 𝑆)
148108, 147sseqtr4d 3621 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ dom 𝐴)
149 simpl1 1062 . . . . . . . . . . . . . . . 16 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → Fun 𝐴)
1501103ad2ant2 1081 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → 𝑦𝑤 (𝑘𝑦) = ran 𝑘)
151 simp3 1061 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ran 𝑘 ⊆ dom 𝐴)
152150, 151eqsstrd 3618 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → 𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
153 iunss 4527 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
154152, 153sylib 208 . . . . . . . . . . . . . . . . 17 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ∀𝑦𝑤 (𝑘𝑦) ⊆ dom 𝐴)
155154r19.21bi 2927 . . . . . . . . . . . . . . . 16 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → (𝑘𝑦) ⊆ dom 𝐴)
156 funimass3 6289 . . . . . . . . . . . . . . . 16 ((Fun 𝐴 ∧ (𝑘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ (𝑘𝑦) ⊆ (𝐴𝑉)))
157149, 155, 156syl2anc 692 . . . . . . . . . . . . . . 15 (((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦𝑤) → ((𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ (𝑘𝑦) ⊆ (𝐴𝑉)))
158157ralbidva 2979 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → (∀𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
159 iunss 4527 . . . . . . . . . . . . . 14 ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 ↔ ∀𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉)
160 iunss 4527 . . . . . . . . . . . . . 14 ( 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉) ↔ ∀𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉))
161158, 159, 1603bitr4g 303 . . . . . . . . . . . . 13 ((Fun 𝐴𝑘 Fn 𝑤 ran 𝑘 ⊆ dom 𝐴) → ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
162145, 146, 148, 161syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ( 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉 𝑦𝑤 (𝑘𝑦) ⊆ (𝐴𝑉)))
163144, 162mpbird 247 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 (𝐴 “ (𝑘𝑦)) ⊆ 𝑉)
164143, 163eqsstr3d 3619 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐴 ran 𝑘) ⊆ 𝑉)
165 imaeq1 5420 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (𝑎 ran 𝑘) = (𝐴 ran 𝑘))
166165sseq1d 3611 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((𝑎 ran 𝑘) ⊆ 𝑉 ↔ (𝐴 ran 𝑘) ⊆ 𝑉))
167166elrab 3346 . . . . . . . . . 10 (𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ↔ (𝐴 ∈ (𝑆 Cn 𝑇) ∧ (𝐴 ran 𝑘) ⊆ 𝑉))
168140, 164, 167sylanbrc 697 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉})
1691ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
170 simprl 793 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) = 𝑤)
171 uniiun 4539 . . . . . . . . . . . 12 𝑤 = 𝑦𝑤 𝑦
172170, 171syl6eq 2671 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) = 𝑦𝑤 𝑦)
173 simpl 473 . . . . . . . . . . . . 13 ((𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)))
174173ralimi 2947 . . . . . . . . . . . 12 (∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp) → ∀𝑦𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)))
175 ss2iun 4502 . . . . . . . . . . . 12 (∀𝑦𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) → 𝑦𝑤 𝑦 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
176116, 174, 1753syl 18 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 𝑦 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
177172, 176eqsstrd 3618 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
178 imaeq1 5420 . . . . . . . . . . . 12 (𝑏 = 𝐵 → (𝑏𝐾) = (𝐵𝐾))
179178sseq1d 3611 . . . . . . . . . . 11 (𝑏 = 𝐵 → ((𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ↔ (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
180179elrab 3346 . . . . . . . . . 10 (𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ↔ (𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝐵𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
181169, 177, 180sylanbrc 697 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})
182 opelxpi 5108 . . . . . . . . 9 ((𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}))
183168, 181, 182syl2anc 692 . . . . . . . 8 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}))
184 imaeq1 5420 . . . . . . . . . . . . . . 15 (𝑎 = 𝑢 → (𝑎 ran 𝑘) = (𝑢 ran 𝑘))
185184sseq1d 3611 . . . . . . . . . . . . . 14 (𝑎 = 𝑢 → ((𝑎 ran 𝑘) ⊆ 𝑉 ↔ (𝑢 ran 𝑘) ⊆ 𝑉))
186185elrab 3346 . . . . . . . . . . . . 13 (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉))
187 imaeq1 5420 . . . . . . . . . . . . . . 15 (𝑏 = 𝑣 → (𝑏𝐾) = (𝑣𝐾))
188187sseq1d 3611 . . . . . . . . . . . . . 14 (𝑏 = 𝑣 → ((𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ↔ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
189188elrab 3346 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))
190186, 189anbi12i 732 . . . . . . . . . . . 12 ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))))
191 simprll 801 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
192 simprrl 803 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
193 coeq1 5239 . . . . . . . . . . . . . . 15 (𝑓 = 𝑢 → (𝑓𝑔) = (𝑢𝑔))
194 coeq2 5240 . . . . . . . . . . . . . . 15 (𝑔 = 𝑣 → (𝑢𝑔) = (𝑢𝑣))
195 xkococn.1 . . . . . . . . . . . . . . 15 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓𝑔))
196 vex 3189 . . . . . . . . . . . . . . . 16 𝑢 ∈ V
197 vex 3189 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
198196, 197coex 7065 . . . . . . . . . . . . . . 15 (𝑢𝑣) ∈ V
199193, 194, 195, 198ovmpt2 6749 . . . . . . . . . . . . . 14 ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢𝑣))
200191, 192, 199syl2anc 692 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝐹𝑣) = (𝑢𝑣))
201 cnco 20980 . . . . . . . . . . . . . . 15 ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢𝑣) ∈ (𝑅 Cn 𝑇))
202192, 191, 201syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝑣) ∈ (𝑅 Cn 𝑇))
203 imaco 5599 . . . . . . . . . . . . . . 15 ((𝑢𝑣) “ 𝐾) = (𝑢 “ (𝑣𝐾))
204 simprrr 804 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)))
20515ntrss2 20771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ Top ∧ (𝑘𝑦) ⊆ 𝑆) → ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦))
206205ex 450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ Top → ((𝑘𝑦) ⊆ 𝑆 → ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦)))
207206ralimdv 2957 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ Top → (∀𝑦𝑤 (𝑘𝑦) ⊆ 𝑆 → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦)))
20890, 130, 207sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦))
209 ss2iun 4502 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ (𝑘𝑦) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ 𝑦𝑤 (𝑘𝑦))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ 𝑦𝑤 (𝑘𝑦))
211210, 111sseqtrd 3620 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ ran 𝑘)
212211adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦)) ⊆ ran 𝑘)
213204, 212sstrd 3593 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑣𝐾) ⊆ ran 𝑘)
214 imass2 5460 . . . . . . . . . . . . . . . . 17 ((𝑣𝐾) ⊆ ran 𝑘 → (𝑢 “ (𝑣𝐾)) ⊆ (𝑢 ran 𝑘))
215213, 214syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 “ (𝑣𝐾)) ⊆ (𝑢 ran 𝑘))
216 simprlr 802 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 ran 𝑘) ⊆ 𝑉)
217215, 216sstrd 3593 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢 “ (𝑣𝐾)) ⊆ 𝑉)
218203, 217syl5eqss 3628 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → ((𝑢𝑣) “ 𝐾) ⊆ 𝑉)
219 imaeq1 5420 . . . . . . . . . . . . . . . 16 ( = (𝑢𝑣) → (𝐾) = ((𝑢𝑣) “ 𝐾))
220219sseq1d 3611 . . . . . . . . . . . . . . 15 ( = (𝑢𝑣) → ((𝐾) ⊆ 𝑉 ↔ ((𝑢𝑣) “ 𝐾) ⊆ 𝑉))
221220elrab 3346 . . . . . . . . . . . . . 14 ((𝑢𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ((𝑢𝑣) ∈ (𝑅 Cn 𝑇) ∧ ((𝑢𝑣) “ 𝐾) ⊆ 𝑉))
222202, 218, 221sylanbrc 697 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
223200, 222eqeltrd 2698 . . . . . . . . . . . 12 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))))) → (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
224190, 223sylan2b 492 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) → (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
225224ralrimivva 2965 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})
226195mpt2fun 6715 . . . . . . . . . . 11 Fun 𝐹
227 ssrab2 3666 . . . . . . . . . . . . 13 {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
228 ssrab2 3666 . . . . . . . . . . . . 13 {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ⊆ (𝑅 Cn 𝑆)
229 xpss12 5186 . . . . . . . . . . . . 13 (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
230227, 228, 229mp2an 707 . . . . . . . . . . . 12 ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
231 vex 3189 . . . . . . . . . . . . . 14 𝑓 ∈ V
232 vex 3189 . . . . . . . . . . . . . 14 𝑔 ∈ V
233231, 232coex 7065 . . . . . . . . . . . . 13 (𝑓𝑔) ∈ V
234195, 233dmmpt2 7185 . . . . . . . . . . . 12 dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
235230, 234sseqtr4i 3617 . . . . . . . . . . 11 ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹
236 funimassov 6764 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))} (𝑢𝐹𝑣) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))
237226, 235, 236mp2an 707 . . . . . . . . . 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 6289 . . . . . . . . . 10 ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})) ⊆ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
240226, 235, 239mp2an 707 . . . . . . . . 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 2687 . . . . . . . . . 10 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))})))
243 sseq1 3605 . . . . . . . . . 10 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → (𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
244242, 243anbi12d 746 . . . . . . . . 9 (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏𝐾) ⊆ 𝑦𝑤 ((int‘𝑆)‘(𝑘𝑦))}) ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
245244rspcev 3295 . . . . . . . 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 1321 . . . . . . 7 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ ((𝐵𝐾) = 𝑤 ∧ (𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉})))
247246expr 642 . . . . . 6 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝐵𝐾) = 𝑤) → ((𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
248247exlimdv 1858 . . . . 5 (((𝜑𝑤 ∈ (𝒫 (𝑆t (𝐵𝐾)) ∩ Fin)) ∧ (𝐵𝐾) = 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (𝐴𝑉) ∧ ∀𝑦𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘𝑦)) ∧ (𝑆t (𝑘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^ko 𝑆) ×t (𝑆 ^ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧𝑧 ⊆ (𝐹 “ { ∈ (𝑅 Cn 𝑇) ∣ (𝐾) ⊆ 𝑉}))))
24989, 248syldan 487 . . . 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 3024 . 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 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cin 3554  wss 3555  𝒫 cpw 4130  cop 4154   cuni 4402   ciun 4485   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cima 5077  ccom 5078  Fun wfun 5841   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  cmpt2 6606  Fincfn 7899  t crest 16002  Topctop 20617  intcnt 20731   Cn ccn 20938  Compccmp 21099  𝑛-Locally cnlly 21178   ×t ctx 21273   ^ko cxko 21274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-fin 7903  df-fi 8261  df-rest 16004  df-topgen 16025  df-top 20621  df-bases 20622  df-topon 20623  df-ntr 20734  df-nei 20812  df-cn 20941  df-cmp 21100  df-nlly 21180  df-tx 21275  df-xko 21276
This theorem is referenced by:  xkococn  21373
  Copyright terms: Public domain W3C validator