MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkoptsub Structured version   Visualization version   GIF version
Theorem xkoptsub 23158
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 22408 . . . . . . . 8 (𝑅 ∈ Top β†’ 𝑋 ∈ 𝑅)
43adantr 482 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝑋 ∈ 𝑅)
5 fconstg 6779 . . . . . . . . 9 (𝑆 ∈ Top β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆ{𝑆})
65adantl 483 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆ{𝑆})
76ffnd 6719 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}) Fn 𝑋)
8 eqid 2733 . . . . . . . 8 {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}
98ptval 23074 . . . . . . 7 ((𝑋 ∈ 𝑅 ∧ (𝑋 Γ— {𝑆}) Fn 𝑋) β†’ (∏tβ€˜(𝑋 Γ— {𝑆})) = (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}))
104, 7, 9syl2anc 585 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (∏tβ€˜(𝑋 Γ— {𝑆})) = (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}))
11 simpr 486 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝑆 ∈ Top)
1211snssd 4813 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {𝑆} βŠ† Top)
136, 12fssd 6736 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— {𝑆}):π‘‹βŸΆTop)
14 eqid 2733 . . . . . . . . . 10 X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)
158, 14ptbasfi 23085 . . . . . . . . 9 ((𝑋 ∈ 𝑅 ∧ (𝑋 Γ— {𝑆}):π‘‹βŸΆTop) β†’ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = (fiβ€˜({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
164, 13, 15syl2anc 585 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = (fiβ€˜({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
17 fvconst2g 7203 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘›) = 𝑆)
1817adantll 713 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘›) = 𝑆)
1918unieqd 4923 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) β†’ βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = βˆͺ 𝑆)
2019ixpeq2dva 8906 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = X𝑛 ∈ 𝑋 βˆͺ 𝑆)
21 eqid 2733 . . . . . . . . . . . . . 14 βˆͺ 𝑆 = βˆͺ 𝑆
2221topopn 22408 . . . . . . . . . . . . 13 (𝑆 ∈ Top β†’ βˆͺ 𝑆 ∈ 𝑆)
23 ixpconstg 8900 . . . . . . . . . . . . 13 ((𝑋 ∈ 𝑅 ∧ βˆͺ 𝑆 ∈ 𝑆) β†’ X𝑛 ∈ 𝑋 βˆͺ 𝑆 = (βˆͺ 𝑆 ↑m 𝑋))
243, 22, 23syl2an 597 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ 𝑆 = (βˆͺ 𝑆 ↑m 𝑋))
2520, 24eqtrd 2773 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = (βˆͺ 𝑆 ↑m 𝑋))
2625sneqd 4641 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} = {(βˆͺ 𝑆 ↑m 𝑋)})
27 eqid 2733 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 7203 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ π‘˜ ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆)
2928adantll 713 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ ((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆)
3025adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) = (βˆͺ 𝑆 ↑m 𝑋))
3130mpteq1d 5244 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)))
3231cnveqd 5876 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)))
3332imaeq1d 6059 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
3433ralrimivw 3151 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
3529, 34jca 513 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘˜ ∈ 𝑋) β†’ (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3635ralrimiva 3147 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ βˆ€π‘˜ ∈ 𝑋 (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
37 mpoeq123 7481 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (((𝑋 Γ— {𝑆})β€˜π‘˜) = 𝑆 ∧ βˆ€π‘’ ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3827, 36, 37sylancr 588 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
3938rneqd 5938 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
4026, 39uneq12d 4165 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) = ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
4140fveq2d 6896 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (fiβ€˜({X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ ((𝑋 Γ— {𝑆})β€˜π‘˜) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝑋 βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) = (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
4216, 41eqtrd 2773 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))} = (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))))
4342fveq2d 6896 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 (π‘”β€˜π‘¦) ∈ ((𝑋 Γ— {𝑆})β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝑋 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((𝑋 Γ— {𝑆})β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝑋 (π‘”β€˜π‘¦))}) = (topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))))
4410, 43eqtrd 2773 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (∏tβ€˜(𝑋 Γ— {𝑆})) = (topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))))
451, 44eqtrid 2785 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝐽 = (topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))))
4645oveq1d 7424 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆)))
47 firest 17378 . . . . 5 (fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆))) = ((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆))
4847fveq2i 6895 . . . 4 (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) = (topGenβ€˜((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆)))
49 fvex 6905 . . . . 5 (fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) ∈ V
50 ovex 7442 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 22663 . . . . 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 691 . . . 4 (topGenβ€˜((fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†Ύt (𝑅 Cn 𝑆))) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆))
5348, 52eqtri 2761 . . 3 (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) = ((topGenβ€˜(fiβ€˜({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))) β†Ύt (𝑅 Cn 𝑆))
5446, 53eqtr4di 2791 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) = (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))))
55 xkotop 23092 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
56 snex 5432 . . . . . 6 {(βˆͺ 𝑆 ↑m 𝑋)} ∈ V
57 mpoexga 8064 . . . . . . . 8 ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
583, 57sylan 581 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
59 rnexg 7895 . . . . . . 7 ((π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V)
61 unexg 7736 . . . . . 6 (({(βˆͺ 𝑆 ↑m 𝑋)} ∈ V ∧ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ∈ V) β†’ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V)
6256, 60, 61sylancr 588 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V)
63 restval 17372 . . . . 5 ((({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) = ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))))
6462, 50, 63sylancl 587 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) = ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))))
65 elun 4149 . . . . . . 7 (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↔ (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} ∨ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
662, 21cnf 22750 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑅 Cn 𝑆) β†’ π‘₯:π‘‹βŸΆβˆͺ 𝑆)
67 elmapg 8833 . . . . . . . . . . . . . . 15 ((βˆͺ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅) β†’ (π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋) ↔ π‘₯:π‘‹βŸΆβˆͺ 𝑆))
6822, 3, 67syl2anr 598 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋) ↔ π‘₯:π‘‹βŸΆβˆͺ 𝑆))
6966, 68imbitrrid 245 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ (𝑅 Cn 𝑆) β†’ π‘₯ ∈ (βˆͺ 𝑆 ↑m 𝑋)))
7069ssrdv 3989 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
7170adantr 482 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
72 elsni 4646 . . . . . . . . . . . 12 (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} β†’ π‘₯ = (βˆͺ 𝑆 ↑m 𝑋))
7372adantl 483 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ π‘₯ = (βˆͺ 𝑆 ↑m 𝑋))
7471, 73sseqtrrd 4024 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) βŠ† π‘₯)
75 sseqin2 4216 . . . . . . . . . 10 ((𝑅 Cn 𝑆) βŠ† π‘₯ ↔ (π‘₯ ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 217 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2733 . . . . . . . . . . . 12 (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
7877xkouni 23103 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) = βˆͺ (𝑆 ↑ko 𝑅))
79 eqid 2733 . . . . . . . . . . . . 13 βˆͺ (𝑆 ↑ko 𝑅) = βˆͺ (𝑆 ↑ko 𝑅)
8079topopn 22408 . . . . . . . . . . . 12 ((𝑆 ↑ko 𝑅) ∈ Top β†’ βˆͺ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
8155, 80syl 17 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ βˆͺ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
8278, 81eqeltrd 2834 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
8382adantr 482 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
8476, 83eqeltrd 2834 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)}) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
85 eqid 2733 . . . . . . . . . . 11 (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
8685rnmpo 7542 . . . . . . . . . 10 ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) = {π‘₯ ∣ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)}
8786eqabri 2878 . . . . . . . . 9 (π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ↔ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
88 cnvresima 6230 . . . . . . . . . . . . . . 15 (β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) β€œ 𝑒) = ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆))
8970adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 Cn 𝑆) βŠ† (βˆͺ 𝑆 ↑m 𝑋))
9089resmptd 6041 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) = (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)))
9190cnveqd 5876 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) = β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)))
9291imaeq1d 6059 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘((𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β†Ύ (𝑅 Cn 𝑆)) β€œ 𝑒) = (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
9388, 92eqtr3id 2787 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) = (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
94 fvex 6905 . . . . . . . . . . . . . . . . . . . 20 (π‘€β€˜π‘˜) ∈ V
9594rgenw 3066 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘€ ∈ (𝑅 Cn 𝑆)(π‘€β€˜π‘˜) ∈ V
96 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))
9796fnmpt 6691 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘€ ∈ (𝑅 Cn 𝑆)(π‘€β€˜π‘˜) ∈ V β†’ (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆))
99 elpreima 7060 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) Fn (𝑅 Cn 𝑆) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒)))
101 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 = 𝑓 β†’ (π‘€β€˜π‘˜) = (π‘“β€˜π‘˜))
102 fvex 6905 . . . . . . . . . . . . . . . . . . . . . 22 (π‘“β€˜π‘˜) ∈ V
103101, 96, 102fvmpt 6999 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) β†’ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) = (π‘“β€˜π‘˜))
104103adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) = (π‘“β€˜π‘˜))
105104eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ (((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒 ↔ (π‘“β€˜π‘˜) ∈ 𝑒))
106102snss 4790 . . . . . . . . . . . . . . . . . . . 20 ((π‘“β€˜π‘˜) ∈ 𝑒 ↔ {(π‘“β€˜π‘˜)} βŠ† 𝑒)
10789sselda 3983 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ 𝑓 ∈ (βˆͺ 𝑆 ↑m 𝑋))
108 elmapi 8843 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ (βˆͺ 𝑆 ↑m 𝑋) β†’ 𝑓:π‘‹βŸΆβˆͺ 𝑆)
109 ffn 6718 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:π‘‹βŸΆβˆͺ 𝑆 β†’ 𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ 𝑓 Fn 𝑋)
111 simplrl 776 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ π‘˜ ∈ 𝑋)
112 fnsnfv 6971 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋 ∧ π‘˜ ∈ 𝑋) β†’ {(π‘“β€˜π‘˜)} = (𝑓 β€œ {π‘˜}))
113110, 111, 112syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ {(π‘“β€˜π‘˜)} = (𝑓 β€œ {π‘˜}))
114113sseq1d 4014 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ({(π‘“β€˜π‘˜)} βŠ† 𝑒 ↔ (𝑓 β€œ {π‘˜}) βŠ† 𝑒))
115106, 114bitrid 283 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ ((π‘“β€˜π‘˜) ∈ 𝑒 ↔ (𝑓 β€œ {π‘˜}) βŠ† 𝑒))
116105, 115bitrd 279 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) β†’ (((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒 ↔ (𝑓 β€œ {π‘˜}) βŠ† 𝑒))
117116pm5.32da 580 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜))β€˜π‘“) ∈ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)))
118100, 117bitrd 279 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑓 ∈ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)))
119118eqabdv 2868 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)})
120 df-rab 3434 . . . . . . . . . . . . . . 15 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 β€œ {π‘˜}) βŠ† 𝑒)}
121119, 120eqtr4di 2791 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (β—‘(𝑀 ∈ (𝑅 Cn 𝑆) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒})
12293, 121eqtrd 2773 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒})
123 simpll 766 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑅 ∈ Top)
12411adantr 482 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑆 ∈ Top)
125 simprl 770 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ π‘˜ ∈ 𝑋)
126125snssd 4813 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ {π‘˜} βŠ† 𝑋)
1272toptopon 22419 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜π‘‹))
128123, 127sylib 217 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑅 ∈ (TopOnβ€˜π‘‹))
129 restsn2 22675 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ π‘˜ ∈ 𝑋) β†’ (𝑅 β†Ύt {π‘˜}) = 𝒫 {π‘˜})
130128, 125, 129syl2anc 585 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 β†Ύt {π‘˜}) = 𝒫 {π‘˜})
131 snfi 9044 . . . . . . . . . . . . . . . 16 {π‘˜} ∈ Fin
132 discmp 22902 . . . . . . . . . . . . . . . 16 ({π‘˜} ∈ Fin ↔ 𝒫 {π‘˜} ∈ Comp)
133131, 132mpbi 229 . . . . . . . . . . . . . . 15 𝒫 {π‘˜} ∈ Comp
134130, 133eqeltrdi 2842 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (𝑅 β†Ύt {π‘˜}) ∈ Comp)
135 simprr 772 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ 𝑒 ∈ 𝑆)
1362, 123, 124, 126, 134, 135xkoopn 23093 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 β€œ {π‘˜}) βŠ† 𝑒} ∈ (𝑆 ↑ko 𝑅))
137122, 136eqeltrd 2834 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138 ineq1 4206 . . . . . . . . . . . . 13 (π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) = ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)))
139138eleq1d 2819 . . . . . . . . . . . 12 (π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ ((π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅) ↔ ((β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
140137, 139syl5ibrcom 246 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘˜ ∈ 𝑋 ∧ 𝑒 ∈ 𝑆)) β†’ (π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
141140rexlimdvva 3212 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
142141imp 408 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ βˆƒπ‘˜ ∈ 𝑋 βˆƒπ‘’ ∈ 𝑆 π‘₯ = (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
14387, 142sylan2b 595 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
14484, 143jaodan 957 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (π‘₯ ∈ {(βˆͺ 𝑆 ↑m 𝑋)} ∨ π‘₯ ∈ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
14565, 144sylan2b 595 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))) β†’ (π‘₯ ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
146145fmpttd 7115 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))):({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))⟢(𝑆 ↑ko 𝑅))
147146frnd 6726 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ ran (π‘₯ ∈ ({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) ↦ (π‘₯ ∩ (𝑅 Cn 𝑆))) βŠ† (𝑆 ↑ko 𝑅))
14864, 147eqsstrd 4021 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅))
149 tgfiss 22494 . . 3 (((𝑆 ↑ko 𝑅) ∈ Top ∧ (({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅)) β†’ (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) βŠ† (𝑆 ↑ko 𝑅))
15055, 148, 149syl2anc 585 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (topGenβ€˜(fiβ€˜(({(βˆͺ 𝑆 ↑m 𝑋)} βˆͺ ran (π‘˜ ∈ 𝑋, 𝑒 ∈ 𝑆 ↦ (β—‘(𝑀 ∈ (βˆͺ 𝑆 ↑m 𝑋) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†Ύt (𝑅 Cn 𝑆)))) βŠ† (𝑆 ↑ko 𝑅))
15154, 150eqsstrd 4021 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐽 β†Ύt (𝑅 Cn 𝑆)) βŠ† (𝑆 ↑ko 𝑅))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411   ↑m cmap 8820  Xcixp 8891  Fincfn 8939  ficfi 9405   β†Ύt crest 17366  topGenctg 17383  βˆtcpt 17384  Topctop 22395  TopOnctopon 22412   Cn ccn 22728  Compccmp 22890   ↑ko cxko 23065
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9406  df-rest 17368  df-topgen 17389  df-pt 17390  df-top 22396  df-topon 22413  df-bases 22449  df-cn 22731  df-cmp 22891  df-xko 23067
This theorem is referenced by:  xkopt  23159  xkopjcn  23160
  Copyright terms: Public domain W3C validator