MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkococnlem Structured version   Visualization version   GIF version
Theorem xkococnlem 23155
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 22893 . . . 4 ((𝐡 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 β†Ύt 𝐾) ∈ Comp) β†’ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∈ Comp)
41, 2, 3syl2anc 585 . . 3 (πœ‘ β†’ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∈ Comp)
5 xkococn.s . . . . . . . . 9 (πœ‘ β†’ 𝑆 ∈ 𝑛-Locally Comp)
65adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ 𝑆 ∈ 𝑛-Locally Comp)
7 xkococn.a . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ (𝑆 Cn 𝑇))
8 xkococn.v . . . . . . . . . 10 (πœ‘ β†’ 𝑉 ∈ 𝑇)
9 cnima 22761 . . . . . . . . . 10 ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) β†’ (◑𝐴 β€œ 𝑉) ∈ 𝑆)
107, 8, 9syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (◑𝐴 β€œ 𝑉) ∈ 𝑆)
1110adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ (◑𝐴 β€œ 𝑉) ∈ 𝑆)
12 imaco 6248 . . . . . . . . . . 11 ((𝐴 ∘ 𝐡) β€œ 𝐾) = (𝐴 β€œ (𝐡 β€œ 𝐾))
13 xkococn.i . . . . . . . . . . 11 (πœ‘ β†’ ((𝐴 ∘ 𝐡) β€œ 𝐾) βŠ† 𝑉)
1412, 13eqsstrrid 4031 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 β€œ (𝐡 β€œ 𝐾)) βŠ† 𝑉)
15 eqid 2733 . . . . . . . . . . . . 13 βˆͺ 𝑆 = βˆͺ 𝑆
16 eqid 2733 . . . . . . . . . . . . 13 βˆͺ 𝑇 = βˆͺ 𝑇
1715, 16cnf 22742 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) β†’ 𝐴:βˆͺ π‘†βŸΆβˆͺ 𝑇)
18 ffun 6718 . . . . . . . . . . . 12 (𝐴:βˆͺ π‘†βŸΆβˆͺ 𝑇 β†’ Fun 𝐴)
197, 17, 183syl 18 . . . . . . . . . . 11 (πœ‘ β†’ Fun 𝐴)
20 imassrn 6069 . . . . . . . . . . . . 13 (𝐡 β€œ 𝐾) βŠ† ran 𝐡
21 eqid 2733 . . . . . . . . . . . . . . 15 βˆͺ 𝑅 = βˆͺ 𝑅
2221, 15cnf 22742 . . . . . . . . . . . . . 14 (𝐡 ∈ (𝑅 Cn 𝑆) β†’ 𝐡:βˆͺ π‘…βŸΆβˆͺ 𝑆)
23 frn 6722 . . . . . . . . . . . . . 14 (𝐡:βˆͺ π‘…βŸΆβˆͺ 𝑆 β†’ ran 𝐡 βŠ† βˆͺ 𝑆)
241, 22, 233syl 18 . . . . . . . . . . . . 13 (πœ‘ β†’ ran 𝐡 βŠ† βˆͺ 𝑆)
2520, 24sstrid 3993 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 β€œ 𝐾) βŠ† βˆͺ 𝑆)
26 fdm 6724 . . . . . . . . . . . . 13 (𝐴:βˆͺ π‘†βŸΆβˆͺ 𝑇 β†’ dom 𝐴 = βˆͺ 𝑆)
277, 17, 263syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ dom 𝐴 = βˆͺ 𝑆)
2825, 27sseqtrrd 4023 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 β€œ 𝐾) βŠ† dom 𝐴)
29 funimass3 7053 . . . . . . . . . . 11 ((Fun 𝐴 ∧ (𝐡 β€œ 𝐾) βŠ† dom 𝐴) β†’ ((𝐴 β€œ (𝐡 β€œ 𝐾)) βŠ† 𝑉 ↔ (𝐡 β€œ 𝐾) βŠ† (◑𝐴 β€œ 𝑉)))
3019, 28, 29syl2anc 585 . . . . . . . . . 10 (πœ‘ β†’ ((𝐴 β€œ (𝐡 β€œ 𝐾)) βŠ† 𝑉 ↔ (𝐡 β€œ 𝐾) βŠ† (◑𝐴 β€œ 𝑉)))
3114, 30mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (𝐡 β€œ 𝐾) βŠ† (◑𝐴 β€œ 𝑉))
3231sselda 3982 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ π‘₯ ∈ (◑𝐴 β€œ 𝑉))
33 nlly2i 22972 . . . . . . . 8 ((𝑆 ∈ 𝑛-Locally Comp ∧ (◑𝐴 β€œ 𝑉) ∈ 𝑆 ∧ π‘₯ ∈ (◑𝐴 β€œ 𝑉)) β†’ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘’ ∈ 𝑆 (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))
346, 11, 32, 33syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘’ ∈ 𝑆 (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))
35 nllytop 22969 . . . . . . . . . . . . 13 (𝑆 ∈ 𝑛-Locally Comp β†’ 𝑆 ∈ Top)
365, 35syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 ∈ Top)
3736ad3antrrr 729 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑆 ∈ Top)
38 imaexg 7903 . . . . . . . . . . . . 13 (𝐡 ∈ (𝑅 Cn 𝑆) β†’ (𝐡 β€œ 𝐾) ∈ V)
391, 38syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 β€œ 𝐾) ∈ V)
4039ad3antrrr 729 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ (𝐡 β€œ 𝐾) ∈ V)
41 simprl 770 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑒 ∈ 𝑆)
42 elrestr 17371 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ (𝐡 β€œ 𝐾) ∈ V ∧ 𝑒 ∈ 𝑆) β†’ (𝑒 ∩ (𝐡 β€œ 𝐾)) ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾)))
4337, 40, 41, 42syl3anc 1372 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑒 ∩ (𝐡 β€œ 𝐾)) ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾)))
44 simprr1 1222 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ π‘₯ ∈ 𝑒)
45 simpllr 775 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ π‘₯ ∈ (𝐡 β€œ 𝐾))
4644, 45elind 4194 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ π‘₯ ∈ (𝑒 ∩ (𝐡 β€œ 𝐾)))
47 inss1 4228 . . . . . . . . . . . 12 (𝑒 ∩ (𝐡 β€œ 𝐾)) βŠ† 𝑒
48 elpwi 4609 . . . . . . . . . . . . . . 15 (𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉) β†’ 𝑠 βŠ† (◑𝐴 β€œ 𝑉))
4948ad2antlr 726 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 βŠ† (◑𝐴 β€œ 𝑉))
50 elssuni 4941 . . . . . . . . . . . . . . . 16 ((◑𝐴 β€œ 𝑉) ∈ 𝑆 β†’ (◑𝐴 β€œ 𝑉) βŠ† βˆͺ 𝑆)
5110, 50syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (◑𝐴 β€œ 𝑉) βŠ† βˆͺ 𝑆)
5251ad3antrrr 729 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ (◑𝐴 β€œ 𝑉) βŠ† βˆͺ 𝑆)
5349, 52sstrd 3992 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 βŠ† βˆͺ 𝑆)
54 simprr2 1223 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑒 βŠ† 𝑠)
5515ssntr 22554 . . . . . . . . . . . . 13 (((𝑆 ∈ Top ∧ 𝑠 βŠ† βˆͺ 𝑆) ∧ (𝑒 ∈ 𝑆 ∧ 𝑒 βŠ† 𝑠)) β†’ 𝑒 βŠ† ((intβ€˜π‘†)β€˜π‘ ))
5637, 53, 41, 54, 55syl22anc 838 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑒 βŠ† ((intβ€˜π‘†)β€˜π‘ ))
5747, 56sstrid 3993 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑒 ∩ (𝐡 β€œ 𝐾)) βŠ† ((intβ€˜π‘†)β€˜π‘ ))
58 simprr3 1224 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑆 β†Ύt 𝑠) ∈ Comp)
5957, 58jca 513 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ ((𝑒 ∩ (𝐡 β€œ 𝐾)) βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))
60 eleq2 2823 . . . . . . . . . . . 12 (𝑦 = (𝑒 ∩ (𝐡 β€œ 𝐾)) β†’ (π‘₯ ∈ 𝑦 ↔ π‘₯ ∈ (𝑒 ∩ (𝐡 β€œ 𝐾))))
61 cleq1lem 14926 . . . . . . . . . . . 12 (𝑦 = (𝑒 ∩ (𝐡 β€œ 𝐾)) β†’ ((𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp) ↔ ((𝑒 ∩ (𝐡 β€œ 𝐾)) βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
6260, 61anbi12d 632 . . . . . . . . . . 11 (𝑦 = (𝑒 ∩ (𝐡 β€œ 𝐾)) β†’ ((π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)) ↔ (π‘₯ ∈ (𝑒 ∩ (𝐡 β€œ 𝐾)) ∧ ((𝑒 ∩ (𝐡 β€œ 𝐾)) βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))))
6362rspcev 3613 . . . . . . . . . 10 (((𝑒 ∩ (𝐡 β€œ 𝐾)) ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∧ (π‘₯ ∈ (𝑒 ∩ (𝐡 β€œ 𝐾)) ∧ ((𝑒 ∩ (𝐡 β€œ 𝐾)) βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
6443, 46, 59, 63syl12anc 836 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) ∧ (𝑒 ∈ 𝑆 ∧ (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
6564rexlimdvaa 3157 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) ∧ 𝑠 ∈ 𝒫 (◑𝐴 β€œ 𝑉)) β†’ (βˆƒπ‘’ ∈ 𝑆 (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp) β†’ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))))
6665reximdva 3169 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ (βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘’ ∈ 𝑆 (π‘₯ ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑆 β†Ύt 𝑠) ∈ Comp) β†’ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))))
6734, 66mpd 15 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
68 rexcom 3288 . . . . . . 7 (βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)) ↔ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
69 r19.42v 3191 . . . . . . . 8 (βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)) ↔ (π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
7069rexbii 3095 . . . . . . 7 (βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)) ↔ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
7168, 70bitri 275 . . . . . 6 (βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)) ↔ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
7267, 71sylib 217 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 β€œ 𝐾)) β†’ βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
7372ralrimiva 3147 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐡 β€œ 𝐾)βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
7415restuni 22658 . . . . . 6 ((𝑆 ∈ Top ∧ (𝐡 β€œ 𝐾) βŠ† βˆͺ 𝑆) β†’ (𝐡 β€œ 𝐾) = βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)))
7536, 25, 74syl2anc 585 . . . . 5 (πœ‘ β†’ (𝐡 β€œ 𝐾) = βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)))
7675raleqdv 3326 . . . 4 (πœ‘ β†’ (βˆ€π‘₯ ∈ (𝐡 β€œ 𝐾)βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)) ↔ βˆ€π‘₯ ∈ βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾))βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))))
7773, 76mpbid 231 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾))βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp)))
78 eqid 2733 . . . 4 βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾))
79 fveq2 6889 . . . . . 6 (𝑠 = (π‘˜β€˜π‘¦) β†’ ((intβ€˜π‘†)β€˜π‘ ) = ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
8079sseq2d 4014 . . . . 5 (𝑠 = (π‘˜β€˜π‘¦) β†’ (𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ↔ 𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))
81 oveq2 7414 . . . . . 6 (𝑠 = (π‘˜β€˜π‘¦) β†’ (𝑆 β†Ύt 𝑠) = (𝑆 β†Ύt (π‘˜β€˜π‘¦)))
8281eleq1d 2819 . . . . 5 (𝑠 = (π‘˜β€˜π‘¦) β†’ ((𝑆 β†Ύt 𝑠) ∈ Comp ↔ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp))
8380, 82anbi12d 632 . . . 4 (𝑠 = (π‘˜β€˜π‘¦) β†’ ((𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp) ↔ (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))
8478, 83cmpcovf 22887 . . 3 (((𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∈ Comp ∧ βˆ€π‘₯ ∈ βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾))βˆƒπ‘¦ ∈ (𝑆 β†Ύt (𝐡 β€œ 𝐾))(π‘₯ ∈ 𝑦 ∧ βˆƒπ‘  ∈ 𝒫 (◑𝐴 β€œ 𝑉)(𝑦 βŠ† ((intβ€˜π‘†)β€˜π‘ ) ∧ (𝑆 β†Ύt 𝑠) ∈ Comp))) β†’ βˆƒπ‘€ ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)(βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ 𝑀 ∧ βˆƒπ‘˜(π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp))))
854, 77, 84syl2anc 585 . 2 (πœ‘ β†’ βˆƒπ‘€ ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)(βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ 𝑀 ∧ βˆƒπ‘˜(π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp))))
8675adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) β†’ (𝐡 β€œ 𝐾) = βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)))
8786eqeq1d 2735 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) β†’ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ↔ βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ 𝑀))
8887biimpar 479 . . . . 5 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ 𝑀) β†’ (𝐡 β€œ 𝐾) = βˆͺ 𝑀)
8936ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝑆 ∈ Top)
90 cntop2 22737 . . . . . . . . . . . 12 (𝐴 ∈ (𝑆 Cn 𝑇) β†’ 𝑇 ∈ Top)
917, 90syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ Top)
9291ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝑇 ∈ Top)
93 xkotop 23084 . . . . . . . . . 10 ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) β†’ (𝑇 ↑ko 𝑆) ∈ Top)
9489, 92, 93syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝑇 ↑ko 𝑆) ∈ Top)
95 cntop1 22736 . . . . . . . . . . . 12 (𝐡 ∈ (𝑅 Cn 𝑆) β†’ 𝑅 ∈ Top)
961, 95syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅 ∈ Top)
9796ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝑅 ∈ Top)
98 xkotop 23084 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
9997, 89, 98syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
100 simprrl 780 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉))
101100frnd 6723 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ ran π‘˜ βŠ† 𝒫 (◑𝐴 β€œ 𝑉))
102 sspwuni 5103 . . . . . . . . . . . 12 (ran π‘˜ βŠ† 𝒫 (◑𝐴 β€œ 𝑉) ↔ βˆͺ ran π‘˜ βŠ† (◑𝐴 β€œ 𝑉))
103101, 102sylib 217 . . . . . . . . . . 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 3992 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ ran π‘˜ βŠ† βˆͺ 𝑆)
107 ffn 6715 . . . . . . . . . . . . 13 (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) β†’ π‘˜ Fn 𝑀)
108 fniunfv 7243 . . . . . . . . . . . . 13 (π‘˜ Fn 𝑀 β†’ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) = βˆͺ ran π‘˜)
109100, 107, 1083syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) = βˆͺ ran π‘˜)
110109oveq2d 7422 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝑆 β†Ύt βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦)) = (𝑆 β†Ύt βˆͺ ran π‘˜))
111 simplr 768 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin))
112111elin2d 4199 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝑀 ∈ Fin)
113 simprrr 781 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp))
114 simpr 486 . . . . . . . . . . . . . 14 ((𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp) β†’ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)
115114ralimi 3084 . . . . . . . . . . . . 13 (βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp) β†’ βˆ€π‘¦ ∈ 𝑀 (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)
116113, 115syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆ€π‘¦ ∈ 𝑀 (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)
11715fiuncmp 22900 . . . . . . . . . . . 12 ((𝑆 ∈ Top ∧ 𝑀 ∈ Fin ∧ βˆ€π‘¦ ∈ 𝑀 (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp) β†’ (𝑆 β†Ύt βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦)) ∈ Comp)
11889, 112, 116, 117syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝑆 β†Ύt βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦)) ∈ Comp)
119110, 118eqeltrrd 2835 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝑆 β†Ύt βˆͺ ran π‘˜) ∈ Comp)
1208ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝑉 ∈ 𝑇)
12115, 89, 92, 106, 119, 120xkoopn 23085 . . . . . . . . 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 4020 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆)
126 iunss 5048 . . . . . . . . . . . . 13 (βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆 ↔ βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆)
127125, 126sylib 217 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆)
12815ntropn 22545 . . . . . . . . . . . . . 14 ((𝑆 ∈ Top ∧ (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆) β†’ ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆)
129128ex 414 . . . . . . . . . . . . 13 (𝑆 ∈ Top β†’ ((π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆 β†’ ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆))
130129ralimdv 3170 . . . . . . . . . . . 12 (𝑆 ∈ Top β†’ (βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆 β†’ βˆ€π‘¦ ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆))
13189, 127, 130sylc 65 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆ€π‘¦ ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆)
132 iunopn 22392 . . . . . . . . . . 11 ((𝑆 ∈ Top ∧ βˆ€π‘¦ ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆) β†’ βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆)
13389, 131, 132syl2anc 585 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∈ 𝑆)
13421, 97, 89, 123, 124, 133xkoopn 23085 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))} ∈ (𝑆 ↑ko 𝑅))
135 txopn 23098 . . . . . . . . 9 ((((𝑇 ↑ko 𝑆) ∈ Top ∧ (𝑆 ↑ko 𝑅) ∈ Top) ∧ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} ∈ (𝑇 ↑ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))} ∈ (𝑆 ↑ko 𝑅))) β†’ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅)))
13694, 99, 121, 134, 135syl22anc 838 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅)))
137 imaeq1 6053 . . . . . . . . . . 11 (π‘Ž = 𝐴 β†’ (π‘Ž β€œ βˆͺ ran π‘˜) = (𝐴 β€œ βˆͺ ran π‘˜))
138137sseq1d 4013 . . . . . . . . . 10 (π‘Ž = 𝐴 β†’ ((π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉 ↔ (𝐴 β€œ βˆͺ ran π‘˜) βŠ† 𝑉))
1397ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝐴 ∈ (𝑆 Cn 𝑇))
140 imaiun 7241 . . . . . . . . . . . 12 (𝐴 β€œ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦)) = βˆͺ 𝑦 ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦))
141109imaeq2d 6058 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝐴 β€œ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦)) = (𝐴 β€œ βˆͺ ran π‘˜))
142140, 141eqtr3id 2787 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) = (𝐴 β€œ βˆͺ ran π‘˜))
143109, 103eqsstrd 4020 . . . . . . . . . . . 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 4023 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ ran π‘˜ βŠ† dom 𝐴)
148 simpl1 1192 . . . . . . . . . . . . . . . 16 (((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) ∧ 𝑦 ∈ 𝑀) β†’ Fun 𝐴)
1491083ad2ant2 1135 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) β†’ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) = βˆͺ ran π‘˜)
150 simp3 1139 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) β†’ βˆͺ ran π‘˜ βŠ† dom 𝐴)
151149, 150eqsstrd 4020 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) β†’ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† dom 𝐴)
152 iunss 5048 . . . . . . . . . . . . . . . . . 18 (βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† dom 𝐴 ↔ βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† dom 𝐴)
153151, 152sylib 217 . . . . . . . . . . . . . . . . 17 ((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) β†’ βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† dom 𝐴)
154153r19.21bi 3249 . . . . . . . . . . . . . . . 16 (((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) ∧ 𝑦 ∈ 𝑀) β†’ (π‘˜β€˜π‘¦) βŠ† dom 𝐴)
155 funimass3 7053 . . . . . . . . . . . . . . . 16 ((Fun 𝐴 ∧ (π‘˜β€˜π‘¦) βŠ† dom 𝐴) β†’ ((𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉 ↔ (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉)))
156148, 154, 155syl2anc 585 . . . . . . . . . . . . . . 15 (((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) ∧ 𝑦 ∈ 𝑀) β†’ ((𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉 ↔ (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉)))
157156ralbidva 3176 . . . . . . . . . . . . . 14 ((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) β†’ (βˆ€π‘¦ ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉 ↔ βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉)))
158 iunss 5048 . . . . . . . . . . . . . 14 (βˆͺ 𝑦 ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉 ↔ βˆ€π‘¦ ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉)
159 iunss 5048 . . . . . . . . . . . . . 14 (βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉) ↔ βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉))
160157, 158, 1593bitr4g 314 . . . . . . . . . . . . 13 ((Fun 𝐴 ∧ π‘˜ Fn 𝑀 ∧ βˆͺ ran π‘˜ βŠ† dom 𝐴) β†’ (βˆͺ 𝑦 ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉 ↔ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉)))
161144, 145, 147, 160syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (βˆͺ 𝑦 ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉 ↔ βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† (◑𝐴 β€œ 𝑉)))
162143, 161mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 (𝐴 β€œ (π‘˜β€˜π‘¦)) βŠ† 𝑉)
163142, 162eqsstrrd 4021 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝐴 β€œ βˆͺ ran π‘˜) βŠ† 𝑉)
164138, 139, 163elrabd 3685 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝐴 ∈ {π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉})
165 imaeq1 6053 . . . . . . . . . . 11 (𝑏 = 𝐡 β†’ (𝑏 β€œ 𝐾) = (𝐡 β€œ 𝐾))
166165sseq1d 4013 . . . . . . . . . 10 (𝑏 = 𝐡 β†’ ((𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ↔ (𝐡 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))
1671ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝐡 ∈ (𝑅 Cn 𝑆))
168 simprl 770 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝐡 β€œ 𝐾) = βˆͺ 𝑀)
169 uniiun 5061 . . . . . . . . . . . 12 βˆͺ 𝑀 = βˆͺ 𝑦 ∈ 𝑀 𝑦
170168, 169eqtrdi 2789 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝐡 β€œ 𝐾) = βˆͺ 𝑦 ∈ 𝑀 𝑦)
171 simpl 484 . . . . . . . . . . . . 13 ((𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp) β†’ 𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
172171ralimi 3084 . . . . . . . . . . . 12 (βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp) β†’ βˆ€π‘¦ ∈ 𝑀 𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
173 ss2iun 5015 . . . . . . . . . . . 12 (βˆ€π‘¦ ∈ 𝑀 𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) β†’ βˆͺ 𝑦 ∈ 𝑀 𝑦 βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
174113, 172, 1733syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 𝑦 βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
175170, 174eqsstrd 4020 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝐡 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
176166, 167, 175elrabd 3685 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ 𝐡 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))})
177164, 176opelxpd 5714 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ ⟨𝐴, 𝐡⟩ ∈ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}))
178 imaeq1 6053 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑒 β†’ (π‘Ž β€œ βˆͺ ran π‘˜) = (𝑒 β€œ βˆͺ ran π‘˜))
179178sseq1d 4013 . . . . . . . . . . . . . 14 (π‘Ž = 𝑒 β†’ ((π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉 ↔ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉))
180179elrab 3683 . . . . . . . . . . . . 13 (𝑒 ∈ {π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} ↔ (𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉))
181 imaeq1 6053 . . . . . . . . . . . . . . 15 (𝑏 = 𝑣 β†’ (𝑏 β€œ 𝐾) = (𝑣 β€œ 𝐾))
182181sseq1d 4013 . . . . . . . . . . . . . 14 (𝑏 = 𝑣 β†’ ((𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ↔ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))
183182elrab 3683 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))
184180, 183anbi12i 628 . . . . . . . . . . . 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 5856 . . . . . . . . . . . . . . 15 (𝑓 = 𝑒 β†’ (𝑓 ∘ 𝑔) = (𝑒 ∘ 𝑔))
188 coeq2 5857 . . . . . . . . . . . . . . 15 (𝑔 = 𝑣 β†’ (𝑒 ∘ 𝑔) = (𝑒 ∘ 𝑣))
189 xkococn.1 . . . . . . . . . . . . . . 15 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
190 vex 3479 . . . . . . . . . . . . . . . 16 𝑒 ∈ V
191 vex 3479 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
192190, 191coex 7918 . . . . . . . . . . . . . . 15 (𝑒 ∘ 𝑣) ∈ V
193187, 188, 189, 192ovmpo 7565 . . . . . . . . . . . . . 14 ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) β†’ (𝑒𝐹𝑣) = (𝑒 ∘ 𝑣))
194185, 186, 193syl2anc 585 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑒𝐹𝑣) = (𝑒 ∘ 𝑣))
195 imaeq1 6053 . . . . . . . . . . . . . . 15 (β„Ž = (𝑒 ∘ 𝑣) β†’ (β„Ž β€œ 𝐾) = ((𝑒 ∘ 𝑣) β€œ 𝐾))
196195sseq1d 4013 . . . . . . . . . . . . . 14 (β„Ž = (𝑒 ∘ 𝑣) β†’ ((β„Ž β€œ 𝐾) βŠ† 𝑉 ↔ ((𝑒 ∘ 𝑣) β€œ 𝐾) βŠ† 𝑉))
197 cnco 22762 . . . . . . . . . . . . . . 15 ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑒 ∈ (𝑆 Cn 𝑇)) β†’ (𝑒 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
198186, 185, 197syl2anc 585 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑒 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
199 imaco 6248 . . . . . . . . . . . . . . 15 ((𝑒 ∘ 𝑣) β€œ 𝐾) = (𝑒 β€œ (𝑣 β€œ 𝐾))
200 simprrr 781 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)))
20115ntrss2 22553 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ Top ∧ (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆) β†’ ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† (π‘˜β€˜π‘¦))
202201ex 414 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ Top β†’ ((π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆 β†’ ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† (π‘˜β€˜π‘¦)))
203202ralimdv 3170 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ Top β†’ (βˆ€π‘¦ ∈ 𝑀 (π‘˜β€˜π‘¦) βŠ† βˆͺ 𝑆 β†’ βˆ€π‘¦ ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† (π‘˜β€˜π‘¦)))
20489, 127, 203sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆ€π‘¦ ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† (π‘˜β€˜π‘¦))
205 ss2iun 5015 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘¦ ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† (π‘˜β€˜π‘¦) β†’ βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† βˆͺ 𝑦 ∈ 𝑀 (π‘˜β€˜π‘¦))
207206, 109sseqtrd 4022 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† βˆͺ ran π‘˜)
208207adantr 482 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) βŠ† βˆͺ ran π‘˜)
209200, 208sstrd 3992 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑣 β€œ 𝐾) βŠ† βˆͺ ran π‘˜)
210 imass2 6099 . . . . . . . . . . . . . . . . 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 3992 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑒 β€œ (𝑣 β€œ 𝐾)) βŠ† 𝑉)
214199, 213eqsstrid 4030 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ ((𝑒 ∘ 𝑣) β€œ 𝐾) βŠ† 𝑉)
215196, 198, 214elrabd 3685 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑒 ∘ 𝑣) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})
216194, 215eqeltrd 2834 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ ((𝑒 ∈ (𝑆 Cn 𝑇) ∧ (𝑒 β€œ βˆͺ ran π‘˜) βŠ† 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))))) β†’ (𝑒𝐹𝑣) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})
217184, 216sylan2b 595 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) ∧ (𝑒 ∈ {π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))})) β†’ (𝑒𝐹𝑣) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})
218217ralrimivva 3201 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆ€π‘’ ∈ {π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉}βˆ€π‘£ ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))} (𝑒𝐹𝑣) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})
219189mpofun 7529 . . . . . . . . . . 11 Fun 𝐹
220 ssrab2 4077 . . . . . . . . . . . . 13 {π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} βŠ† (𝑆 Cn 𝑇)
221 ssrab2 4077 . . . . . . . . . . . . 13 {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))} βŠ† (𝑅 Cn 𝑆)
222 xpss12 5691 . . . . . . . . . . . . 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 3479 . . . . . . . . . . . . . 14 𝑓 ∈ V
225 vex 3479 . . . . . . . . . . . . . 14 𝑔 ∈ V
226224, 225coex 7918 . . . . . . . . . . . . 13 (𝑓 ∘ 𝑔) ∈ V
227189, 226dmmpo 8054 . . . . . . . . . . . 12 dom 𝐹 = ((𝑆 Cn 𝑇) Γ— (𝑅 Cn 𝑆))
228223, 227sseqtrri 4019 . . . . . . . . . . 11 ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) βŠ† dom 𝐹
229 funimassov 7581 . . . . . . . . . . 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 233 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ (𝐹 β€œ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))})) βŠ† {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})
232 funimass3 7053 . . . . . . . . . 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 217 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}))
235 eleq2 2823 . . . . . . . . . 10 (𝑧 = ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) β†’ (⟨𝐴, 𝐡⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐡⟩ ∈ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))})))
236 sseq1 4007 . . . . . . . . . 10 (𝑧 = ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) β†’ (𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}) ↔ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})))
237235, 236anbi12d 632 . . . . . . . . 9 (𝑧 = ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) β†’ ((⟨𝐴, 𝐡⟩ ∈ 𝑧 ∧ 𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})) ↔ (⟨𝐴, 𝐡⟩ ∈ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) ∧ ({π‘Ž ∈ (𝑆 Cn 𝑇) ∣ (π‘Ž β€œ βˆͺ ran π‘˜) βŠ† 𝑉} Γ— {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 β€œ 𝐾) βŠ† βˆͺ 𝑦 ∈ 𝑀 ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦))}) βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}))))
238237rspcev 3613 . . . . . . . 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 836 . . . . . . 7 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ ((𝐡 β€œ 𝐾) = βˆͺ 𝑀 ∧ (π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)))) β†’ βˆƒπ‘§ ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅))(⟨𝐴, 𝐡⟩ ∈ 𝑧 ∧ 𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉})))
240239expr 458 . . . . . 6 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ (𝐡 β€œ 𝐾) = βˆͺ 𝑀) β†’ ((π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)) β†’ βˆƒπ‘§ ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅))(⟨𝐴, 𝐡⟩ ∈ 𝑧 ∧ 𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}))))
241240exlimdv 1937 . . . . 5 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ (𝐡 β€œ 𝐾) = βˆͺ 𝑀) β†’ (βˆƒπ‘˜(π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)) β†’ βˆƒπ‘§ ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅))(⟨𝐴, 𝐡⟩ ∈ 𝑧 ∧ 𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}))))
24288, 241syldan 592 . . . 4 (((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) ∧ βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ 𝑀) β†’ (βˆƒπ‘˜(π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp)) β†’ βˆƒπ‘§ ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅))(⟨𝐴, 𝐡⟩ ∈ 𝑧 ∧ 𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}))))
243242expimpd 455 . . 3 ((πœ‘ ∧ 𝑀 ∈ (𝒫 (𝑆 β†Ύt (𝐡 β€œ 𝐾)) ∩ Fin)) β†’ ((βˆͺ (𝑆 β†Ύt (𝐡 β€œ 𝐾)) = βˆͺ 𝑀 ∧ βˆƒπ‘˜(π‘˜:π‘€βŸΆπ’« (◑𝐴 β€œ 𝑉) ∧ βˆ€π‘¦ ∈ 𝑀 (𝑦 βŠ† ((intβ€˜π‘†)β€˜(π‘˜β€˜π‘¦)) ∧ (𝑆 β†Ύt (π‘˜β€˜π‘¦)) ∈ Comp))) β†’ βˆƒπ‘§ ∈ ((𝑇 ↑ko 𝑆) Γ—t (𝑆 ↑ko 𝑅))(⟨𝐴, 𝐡⟩ ∈ 𝑧 ∧ 𝑧 βŠ† (◑𝐹 β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ 𝐾) βŠ† 𝑉}))))
244243rexlimdva 3156 . 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 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   ∩ cin 3947   βŠ† wss 3948  π’« cpw 4602  βŸ¨cop 4634  βˆͺ cuni 4908  βˆͺ ciun 4997   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β€œ cima 5679   ∘ ccom 5680  Fun wfun 6535   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ∈ cmpo 7408  Fincfn 8936   β†Ύt crest 17363  Topctop 22387  intcnt 22513   Cn ccn 22720  Compccmp 22882  π‘›-Locally cnlly 22961   Γ—t ctx 23056   ↑ko cxko 23057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-1o 8463  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-fin 8940  df-fi 9403  df-rest 17365  df-topgen 17386  df-top 22388  df-topon 22405  df-bases 22441  df-ntr 22516  df-nei 22594  df-cn 22723  df-cmp 22883  df-nlly 22963  df-tx 23058  df-xko 23059
This theorem is referenced by:  xkococn  23156
  Copyright terms: Public domain W3C validator