MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkoptsub Structured version   Visualization version   GIF version
Theorem xkoptsub 23149
Description: The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
Hypotheses
Ref Expression
xkoptsub.x 𝑋 = βˆͺ 𝑅
xkoptsub.j 𝐽 = (∏tβ€˜(𝑋 Γ— {𝑆}))
Assertion
Ref Expression
xkoptsub ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅))
Proof of Theorem xkoptsub
Dummy variables 𝑓 𝑔 π‘˜ 𝑛 𝑒 𝑀 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkoptsub.j . . . . 5 𝐽 = (∏tβ€˜(𝑋 Γ— {𝑆}))
2 xkoptsub.x . . . . . . . . 9 𝑋 = βˆͺ 𝑅
32topopn 22399 . . . . . . . 8 (𝑅 ∈ Top β†’ 𝑋 ∈ 𝑅)
43adantr 481 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝑋 ∈ 𝑅)
5 fconstg 6775 . . . . . . . . 9 (𝑆 ∈ Top β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆ{𝑆})
65adantl 482 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆ{𝑆})
76ffnd 6715 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}) Fn 𝑋)
8 eqid 2732 . . . . . . . 8 {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}
98ptval 23065 . . . . . . 7 ((𝑋 ∈ 𝑅 ∧ (𝑋 Γ— {𝑆}) Fn 𝑋) β†’ (∏tβ€˜(𝑋 Γ— {𝑆})) = (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}))
104, 7, 9syl2anc 584 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (∏tβ€˜(𝑋 Γ— {𝑆})) = (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}))
11 simpr 485 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝑆 ∈ Top)
1211snssd 4811 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {𝑆} βŠ† Top)
136, 12fssd 6732 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆTop)
14 eqid 2732 . . . . . . . . . 10 X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)
158, 14ptbasfi 23076 . . . . . . . . 9 ((𝑋 ∈ 𝑅 ∧ (𝑋 Γ— {𝑆}):π‘‹βŸΆTop) β†’ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = (fiβ€˜({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
164, 13, 15syl2anc 584 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = (fiβ€˜({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
17 fvconst2g 7199 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘›) = 𝑆)
1817adantll 712 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘›) = 𝑆)
1918unieqd 4921 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) β†’ βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = βˆͺ 𝑆)
2019ixpeq2dva 8902 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = X𝑛 ∈ 𝑋 βˆͺ 𝑆)
21 eqid 2732 . . . . . . . . . . . . . 14 βˆͺ 𝑆 = βˆͺ 𝑆
2221topopn 22399 . . . . . . . . . . . . 13 (𝑆 ∈ Top β†’ βˆͺ 𝑆 ∈ 𝑆)
23 ixpconstg 8896 . . . . . . . . . . . . 13 ((𝑋 ∈ 𝑅 ∧ βˆͺ 𝑆 ∈ 𝑆) β†’ X𝑛 ∈ 𝑋 βˆͺ 𝑆 = (βˆͺ 𝑆 ↑m 𝑋))
243, 22, 23syl2an 596 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ 𝑆 = (βˆͺ 𝑆 ↑m 𝑋))
2520, 24eqtrd 2772 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = (βˆͺ 𝑆 ↑m 𝑋))
2625sneqd 4639 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} = {(βˆͺ 𝑆 ↑m 𝑋)})
27 eqid 2732 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 7199 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ π‘˜ ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆)
2928adantll 712 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆)
3025adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = (βˆͺ 𝑆 ↑m 𝑋))
3130mpteq1d 5242 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)))
3231cnveqd 5873 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)))
3332imaeq1d 6056 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
3433ralrimivw 3150 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
3529, 34jca 512 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3635ralrimiva 3146 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ βˆ€π‘˜ ∈ 𝑋 (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
37 mpoeq123 7477 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3827, 36, 37sylancr 587 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3938rneqd 5935 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
4026, 39uneq12d 4163 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) = ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
4140fveq2d 6892 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (fiβ€˜({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) = (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
4216, 41eqtrd 2772 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
4342fveq2d 6892 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}) = (topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))))
4410, 43eqtrd 2772 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (∏tβ€˜(𝑋 Γ— {𝑆})) = (topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))))
451, 44eqtrid 2784 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝐽 = (topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))))
4645oveq1d 7420 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆)))
47 firest 17374 . . . . 5 (fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆))) = ((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆))
4847fveq2i 6891 . . . 4 (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) = (topGenβ€˜((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆)))
49 fvex 6901 . . . . 5 (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) ∈ V
50 ovex 7438 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 22654 . . . . 5 (((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) β†’ (topGenβ€˜((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆))) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆)))
5249, 50, 51mp2an 690 . . . 4 (topGenβ€˜((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆))) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆))
5348, 52eqtri 2760 . . 3 (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆))
5446, 53eqtr4di 2790 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) = (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))))
55 xkotop 23083 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
56 snex 5430 . . . . . 6 {(βˆͺ 𝑆 ↑m 𝑋)} ∈ V
57 mpoexga 8060 . . . . . . . 8 ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
583, 57sylan 580 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
59 rnexg 7891 . . . . . . 7 ((π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
61 unexg 7732 . . . . . 6 (({(βˆͺ 𝑆 ↑m 𝑋)} ∈ V ∧ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V) β†’ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V)
6256, 60, 61sylancr 587 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V)
63 restval 17368 . . . . 5 ((({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) = ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))))
6462, 50, 63sylancl 586 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) = ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))))
65 elun 4147 . . . . . . 7 (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↔ (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} ∨ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
662, 21cnf 22741 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑅 Cn 𝑆) β†’ π‘₯:π‘‹βŸΆβˆͺ 𝑆)
67 elmapg 8829 . . . . . . . . . . . . . . 15 ((βˆͺ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅) β†’ (π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋) ↔ π‘₯:π‘‹βŸΆβˆͺ 𝑆))
6822, 3, 67syl2anr 597 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋) ↔ π‘₯:π‘‹βŸΆβˆͺ 𝑆))
6966, 68imbitrrid 245 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ (𝑅 Cn 𝑆) β†’ π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋)))
7069ssrdv 3987 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
7170adantr 481 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
72 elsni 4644 . . . . . . . . . . . 12 (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} β†’ π‘₯ = (βˆͺ 𝑆 ↑m 𝑋))
7372adantl 482 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ π‘₯ = (βˆͺ 𝑆 ↑m 𝑋))
7471, 73sseqtrrd 4022 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) βŠ† π‘₯)
75 sseqin2 4214 . . . . . . . . . 10 ((𝑅 Cn 𝑆) βŠ† π‘₯ ↔ (π‘₯ ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 217 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2732 . . . . . . . . . . . 12 (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
7877xkouni 23094 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) = βˆͺ (𝑆 ↑ko 𝑅))
79 eqid 2732 . . . . . . . . . . . . 13 βˆͺ (𝑆 ↑ko 𝑅) = βˆͺ (𝑆 ↑ko 𝑅)
8079topopn 22399 . . . . . . . . . . . 12 ((𝑆 ↑ko 𝑅) ∈ Top β†’ βˆͺ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
8155, 80syl 17 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ βˆͺ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
8278, 81eqeltrd 2833 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
8382adantr 481 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
8476, 83eqeltrd 2833 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
85 eqid 2732 . . . . . . . . . . 11 (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
8685rnmpo 7538 . . . . . . . . . 10 ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = {π‘₯ ∣ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)}
8786eqabri 2877 . . . . . . . . 9 (π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ↔ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
88 cnvresima 6226 . . . . . . . . . . . . . . 15 (β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) β€œ 𝑒) = ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆))
8970adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
9089resmptd 6038 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) = (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)))
9190cnveqd 5873 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) = β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)))
9291imaeq1d 6056 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) β€œ 𝑒) = (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
9388, 92eqtr3id 2786 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) = (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
94 fvex 6901 . . . . . . . . . . . . . . . . . . . 20 (π‘€β€˜π‘˜) ∈ V
9594rgenw 3065 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘€ ∈ (𝑅 Cn 𝑆)(π‘€β€˜π‘˜) ∈ V
96 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))
9796fnmpt 6687 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘€ ∈ (𝑅 Cn 𝑆)(π‘€β€˜π‘˜) ∈ V β†’ (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆))
99 elpreima 7056 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒)))
101 fveq1 6887 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = 𝑓 β†’ (π‘€β€˜π‘˜) = (π‘“β€˜π‘˜))
102 fvex 6901 . . . . . . . . . . . . . . . . . . . . . 22 (π‘“β€˜π‘˜) ∈ V
103101, 96, 102fvmpt 6995 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) β†’ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) = (π‘“β€˜π‘˜))
104103adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) = (π‘“β€˜π‘˜))
105104eleq1d 2818 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ (((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒 ↔ (π‘“β€˜π‘˜) ∈ 𝑒))
106102snss 4788 . . . . . . . . . . . . . . . . . . . 20 ((π‘“β€˜π‘˜) ∈ 𝑒 ↔ {(π‘“β€˜π‘˜)} βŠ† 𝑒)
10789sselda 3981 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ 𝑓 ∈ (βˆͺ 𝑆 ↑m 𝑋))
108 elmapi 8839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ (βˆͺ 𝑆 ↑m 𝑋) β†’ 𝑓:π‘‹βŸΆβˆͺ 𝑆)
109 ffn 6714 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:π‘‹βŸΆβˆͺ 𝑆 β†’ 𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ 𝑓 Fn 𝑋)
111 simplrl 775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ π‘˜ ∈ 𝑋)
112 fnsnfv 6967 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋 ∧ π‘˜ ∈ 𝑋) β†’ {(π‘“β€˜π‘˜)} = (𝑓 β€œ {π‘˜}))
113110, 111, 112syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ {(π‘“β€˜π‘˜)} = (𝑓 β€œ {π‘˜}))
114113sseq1d 4012 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ({(π‘“β€˜π‘˜)} βŠ† 𝑒 ↔ (𝑓 β€œ {π‘˜}) βŠ† 𝑒))
115106, 114bitrid 282 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ((π‘“β€˜π‘˜) ∈ 𝑒 ↔ (𝑓 β€œ {π‘˜}) βŠ† 𝑒))
116105, 115bitrd 278 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ (((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒 ↔ (𝑓 β€œ {π‘˜}) βŠ† 𝑒))
117116pm5.32da 579 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)))
118100, 117bitrd 278 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)))
119118eqabdv 2867 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)})
120 df-rab 3433 . . . . . . . . . . . . . . 15 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)}
121119, 120eqtr4di 2790 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒})
12293, 121eqtrd 2772 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒})
123 simpll 765 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑅 ∈ Top)
12411adantr 481 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑆 ∈ Top)
125 simprl 769 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ π‘˜ ∈ 𝑋)
126125snssd 4811 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ {π‘˜} βŠ† 𝑋)
1272toptopon 22410 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜π‘‹))
128123, 127sylib 217 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑅 ∈ (TopOnβ€˜π‘‹))
129 restsn2 22666 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ π‘˜ ∈ 𝑋) β†’ (𝑅 β†Ύt {π‘˜}) = 𝒫 {π‘˜})
130128, 125, 129syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 β†Ύt {π‘˜}) = 𝒫 {π‘˜})
131 snfi 9040 . . . . . . . . . . . . . . . 16 {π‘˜} ∈ Fin
132 discmp 22893 . . . . . . . . . . . . . . . 16 ({π‘˜} ∈ Fin ↔ 𝒫 {π‘˜} ∈ Comp)
133131, 132mpbi 229 . . . . . . . . . . . . . . 15 𝒫 {π‘˜} ∈ Comp
134130, 133eqeltrdi 2841 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 β†Ύt {π‘˜}) ∈ Comp)
135 simprr 771 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑒 ∈ 𝑆)
1362, 123, 124, 126, 134, 135xkoopn 23084 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒} ∈ (𝑆 ↑ko 𝑅))
137122, 136eqeltrd 2833 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138 ineq1 4204 . . . . . . . . . . . . 13 (π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) = ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)))
139138eleq1d 2818 . . . . . . . . . . . 12 (π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ ((π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅) ↔ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
140137, 139syl5ibrcom 246 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
141140rexlimdvva 3211 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
142141imp 407 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
14387, 142sylan2b 594 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
14484, 143jaodan 956 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} ∨ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
14565, 144sylan2b 594 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
146145fmpttd 7111 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))):({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))⟢(𝑆 ↑ko 𝑅))
147146frnd 6722 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))) βŠ† (𝑆 ↑ko 𝑅))
14864, 147eqsstrd 4019 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅))
149 tgfiss 22485 . . 3 (((𝑆 ↑ko 𝑅) ∈ Top ∧ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅)) β†’ (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) βŠ† (𝑆 ↑ko 𝑅))
15055, 148, 149syl2anc 584 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) βŠ† (𝑆 ↑ko 𝑅))
15154, 150eqsstrd 4019 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   ↦ cmpt 5230   Γ— cxp 5673  β—‘ccnv 5674  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407   ↑m cmap 8816  Xcixp 8887  Fincfn 8935  ficfi 9401   β†Ύt crest 17362  topGenctg 17379  βˆtcpt 17380  Topctop 22386  TopOnctopon 22403   Cn ccn 22719  Compccmp 22881   ↑ko cxko 23056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-1o 8462  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-fin 8939  df-fi 9402  df-rest 17364  df-topgen 17385  df-pt 17386  df-top 22387  df-topon 22404  df-bases 22440  df-cn 22722  df-cmp 22882  df-xko 23058
This theorem is referenced by:  xkopt  23150  xkopjcn  23151
  Copyright terms: Public domain W3C validator