MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkoptsub Structured version   Visualization version   GIF version
Theorem xkoptsub 23165
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 22415 . . . . . . . 8 (𝑅 ∈ Top β†’ 𝑋 ∈ 𝑅)
43adantr 481 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝑋 ∈ 𝑅)
5 fconstg 6778 . . . . . . . . 9 (𝑆 ∈ Top β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆ{𝑆})
65adantl 482 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆ{𝑆})
76ffnd 6718 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}) Fn 𝑋)
8 eqid 2732 . . . . . . . 8 {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}
98ptval 23081 . . . . . . 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 4812 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {𝑆} βŠ† Top)
136, 12fssd 6735 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆTop)
14 eqid 2732 . . . . . . . . . 10 X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)
158, 14ptbasfi 23092 . . . . . . . . 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 7205 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘›) = 𝑆)
1817adantll 712 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘›) = 𝑆)
1918unieqd 4922 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) β†’ βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = βˆͺ 𝑆)
2019ixpeq2dva 8908 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = X𝑛 ∈ 𝑋 βˆͺ 𝑆)
21 eqid 2732 . . . . . . . . . . . . . 14 βˆͺ 𝑆 = βˆͺ 𝑆
2221topopn 22415 . . . . . . . . . . . . 13 (𝑆 ∈ Top β†’ βˆͺ 𝑆 ∈ 𝑆)
23 ixpconstg 8902 . . . . . . . . . . . . 13 ((𝑋 ∈ 𝑅 ∧ βˆͺ 𝑆 ∈ 𝑆) β†’ X𝑛 ∈ 𝑋 βˆͺ 𝑆 = (βˆͺ 𝑆 ↑m 𝑋))
243, 22, 23syl2an 596 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ 𝑆 = (βˆͺ 𝑆 ↑m 𝑋))
2520, 24eqtrd 2772 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = (βˆͺ 𝑆 ↑m 𝑋))
2625sneqd 4640 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} = {(βˆͺ 𝑆 ↑m 𝑋)})
27 eqid 2732 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 7205 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ π‘˜ ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆)
2928adantll 712 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆)
3025adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = (βˆͺ 𝑆 ↑m 𝑋))
3130mpteq1d 5243 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)))
3231cnveqd 5875 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)))
3332imaeq1d 6058 . . . . . . . . . . . . . . 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 7483 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3827, 36, 37sylancr 587 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3938rneqd 5937 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
4026, 39uneq12d 4164 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) = ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
4140fveq2d 6895 . . . . . . . 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 6895 . . . . . 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 7426 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆)))
47 firest 17380 . . . . 5 (fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆))) = ((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆))
4847fveq2i 6894 . . . 4 (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) = (topGenβ€˜((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆)))
49 fvex 6904 . . . . 5 (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) ∈ V
50 ovex 7444 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 22670 . . . . 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 23099 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
56 snex 5431 . . . . . 6 {(βˆͺ 𝑆 ↑m 𝑋)} ∈ V
57 mpoexga 8066 . . . . . . . 8 ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
583, 57sylan 580 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
59 rnexg 7897 . . . . . . 7 ((π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
61 unexg 7738 . . . . . 6 (({(βˆͺ 𝑆 ↑m 𝑋)} ∈ V ∧ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V) β†’ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V)
6256, 60, 61sylancr 587 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V)
63 restval 17374 . . . . 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 4148 . . . . . . 7 (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↔ (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} ∨ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
662, 21cnf 22757 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑅 Cn 𝑆) β†’ π‘₯:π‘‹βŸΆβˆͺ 𝑆)
67 elmapg 8835 . . . . . . . . . . . . . . 15 ((βˆͺ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅) β†’ (π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋) ↔ π‘₯:π‘‹βŸΆβˆͺ 𝑆))
6822, 3, 67syl2anr 597 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋) ↔ π‘₯:π‘‹βŸΆβˆͺ 𝑆))
6966, 68imbitrrid 245 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ (𝑅 Cn 𝑆) β†’ π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋)))
7069ssrdv 3988 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
7170adantr 481 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
72 elsni 4645 . . . . . . . . . . . 12 (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} β†’ π‘₯ = (βˆͺ 𝑆 ↑m 𝑋))
7372adantl 482 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ π‘₯ = (βˆͺ 𝑆 ↑m 𝑋))
7471, 73sseqtrrd 4023 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) βŠ† π‘₯)
75 sseqin2 4215 . . . . . . . . . 10 ((𝑅 Cn 𝑆) βŠ† π‘₯ ↔ (π‘₯ ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 217 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2732 . . . . . . . . . . . 12 (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
7877xkouni 23110 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) = βˆͺ (𝑆 ↑ko 𝑅))
79 eqid 2732 . . . . . . . . . . . . 13 βˆͺ (𝑆 ↑ko 𝑅) = βˆͺ (𝑆 ↑ko 𝑅)
8079topopn 22415 . . . . . . . . . . . 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 7544 . . . . . . . . . 10 ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = {π‘₯ ∣ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)}
8786eqabri 2877 . . . . . . . . 9 (π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ↔ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
88 cnvresima 6229 . . . . . . . . . . . . . . 15 (β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) β€œ 𝑒) = ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆))
8970adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
9089resmptd 6040 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) = (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)))
9190cnveqd 5875 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) = β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)))
9291imaeq1d 6058 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) β€œ 𝑒) = (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
9388, 92eqtr3id 2786 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) = (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
94 fvex 6904 . . . . . . . . . . . . . . . . . . . 20 (π‘€β€˜π‘˜) ∈ V
9594rgenw 3065 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘€ ∈ (𝑅 Cn 𝑆)(π‘€β€˜π‘˜) ∈ V
96 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))
9796fnmpt 6690 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘€ ∈ (𝑅 Cn 𝑆)(π‘€β€˜π‘˜) ∈ V β†’ (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆))
99 elpreima 7059 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒)))
101 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = 𝑓 β†’ (π‘€β€˜π‘˜) = (π‘“β€˜π‘˜))
102 fvex 6904 . . . . . . . . . . . . . . . . . . . . . 22 (π‘“β€˜π‘˜) ∈ V
103101, 96, 102fvmpt 6998 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) β†’ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) = (π‘“β€˜π‘˜))
104103adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) = (π‘“β€˜π‘˜))
105104eleq1d 2818 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ (((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒 ↔ (π‘“β€˜π‘˜) ∈ 𝑒))
106102snss 4789 . . . . . . . . . . . . . . . . . . . 20 ((π‘“β€˜π‘˜) ∈ 𝑒 ↔ {(π‘“β€˜π‘˜)} βŠ† 𝑒)
10789sselda 3982 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ 𝑓 ∈ (βˆͺ 𝑆 ↑m 𝑋))
108 elmapi 8845 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ (βˆͺ 𝑆 ↑m 𝑋) β†’ 𝑓:π‘‹βŸΆβˆͺ 𝑆)
109 ffn 6717 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:π‘‹βŸΆβˆͺ 𝑆 β†’ 𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ 𝑓 Fn 𝑋)
111 simplrl 775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ π‘˜ ∈ 𝑋)
112 fnsnfv 6970 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋 ∧ π‘˜ ∈ 𝑋) β†’ {(π‘“β€˜π‘˜)} = (𝑓 β€œ {π‘˜}))
113110, 111, 112syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ {(π‘“β€˜π‘˜)} = (𝑓 β€œ {π‘˜}))
114113sseq1d 4013 . . . . . . . . . . . . . . . . . . . 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 4812 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ {π‘˜} βŠ† 𝑋)
1272toptopon 22426 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜π‘‹))
128123, 127sylib 217 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑅 ∈ (TopOnβ€˜π‘‹))
129 restsn2 22682 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ π‘˜ ∈ 𝑋) β†’ (𝑅 β†Ύt {π‘˜}) = 𝒫 {π‘˜})
130128, 125, 129syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 β†Ύt {π‘˜}) = 𝒫 {π‘˜})
131 snfi 9046 . . . . . . . . . . . . . . . 16 {π‘˜} ∈ Fin
132 discmp 22909 . . . . . . . . . . . . . . . 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 23100 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒} ∈ (𝑆 ↑ko 𝑅))
137122, 136eqeltrd 2833 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138 ineq1 4205 . . . . . . . . . . . . 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 7116 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))):({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))⟢(𝑆 ↑ko 𝑅))
147146frnd 6725 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))) βŠ† (𝑆 ↑ko 𝑅))
14864, 147eqsstrd 4020 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅))
149 tgfiss 22501 . . 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 4020 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 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413   ↑m cmap 8822  Xcixp 8893  Fincfn 8941  ficfi 9407   β†Ύt crest 17368  topGenctg 17385  βˆtcpt 17386  Topctop 22402  TopOnctopon 22419   Cn ccn 22735  Compccmp 22897   ↑ko cxko 23072
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 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-iin 5000  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 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-rest 17370  df-topgen 17391  df-pt 17392  df-top 22403  df-topon 22420  df-bases 22456  df-cn 22738  df-cmp 22898  df-xko 23074
This theorem is referenced by:  xkopt  23166  xkopjcn  23167
  Copyright terms: Public domain W3C validator