Theorem xkoptsub 23678

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.

Step	Hyp	Ref	Expression
1		xkoptsub.j	. . . . 5 ⊢ 𝐽 = (∏t‘(𝑋 × {𝑆}))
2		xkoptsub.x	. . . . . . . . 9 ⊢ 𝑋 = ∪ 𝑅
3	2	topopn 22928	. . . . . . . 8 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
4	3	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋 ∈ 𝑅)
5		fconstg 6796	. . . . . . . . 9 ⊢ (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
6	5	adantl 481	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
7	6	ffnd 6738	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8		eqid 2735	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}
9	8	ptval 23594	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}))
10	4, 7, 9	syl2anc 584	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}))
11		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
12	11	snssd 4814	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
13	6, 12	fssd 6754	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14		eqid 2735	. . . . . . . . . 10 ⊢ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)
15	8, 14	ptbasfi 23605	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))))
16	4, 13, 15	syl2anc 584	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))))
17		fvconst2g 7222	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
18	17	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
19	18	unieqd 4925	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ∪ ((𝑋 × {𝑆})‘𝑛) = ∪ 𝑆)
20	19	ixpeq2dva 8951	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ 𝑆)
21		eqid 2735	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑆 = ∪ 𝑆
22	21	topopn 22928	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆)
23		ixpconstg 8945	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
24	3, 22, 23	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
25	20, 24	eqtrd 2775	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
26	25	sneqd 4643	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} = {(∪ 𝑆 ↑m 𝑋)})
27		eqid 2735	. . . . . . . . . . . 12 ⊢ 𝑋 = 𝑋
28		fvconst2g 7222	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
29	28	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
30	25	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
31	30	mpteq1d 5243	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
32	31	cnveqd 5889	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
33	32	imaeq1d 6079	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
34	33	ralrimivw 3148	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
35	29, 34	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
36	35	ralrimiva 3144	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
37		mpoeq123 7505	. . . . . . . . . . . 12 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
38	27, 36, 37	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
39	38	rneqd 5952	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
40	26, 39	uneq12d 4179	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))) = ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
41	40	fveq2d 6911	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))) = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
42	16, 41	eqtrd 2775	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
43	42	fveq2d 6911	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
44	10, 43	eqtrd 2775	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
45	1, 44	eqtrid 2787	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
46	45	oveq1d 7446	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47		firest 17479	. . . . 5 ⊢ (fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
48	47	fveq2i 6910	. . . 4 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49		fvex 6920	. . . . 5 ⊢ (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V
50		ovex 7464	. . . . 5 ⊢ (𝑅 Cn 𝑆) ∈ V
51		tgrest 23183	. . . . 5 ⊢ (((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
52	49, 50, 51	mp2an 692	. . . 4 ⊢ (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
53	48, 52	eqtri 2763	. . 3 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
54	46, 53	eqtr4di 2793	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55		xkotop 23612	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
56		snex 5442	. . . . . 6 ⊢ {(∪ 𝑆 ↑m 𝑋)} ∈ V
57		mpoexga 8101	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
58	3, 57	sylan 580	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
59		rnexg 7925	. . . . . . 7 ⊢ ((𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
60	58, 59	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
61		unexg 7762	. . . . . 6 ⊢ (({(∪ 𝑆 ↑m 𝑋)} ∈ V ∧ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
62	56, 60, 61	sylancr 587	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
63		restval 17473	. . . . 5 ⊢ ((({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
64	62, 50, 63	sylancl 586	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
65		elun 4163	. . . . . . 7 ⊢ (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
66	2, 21	cnf 23270	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋⟶∪ 𝑆)
67		elmapg 8878	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅) → (𝑥 ∈ (∪ 𝑆 ↑m 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆))
68	22, 3, 67	syl2anr 597	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (∪ 𝑆 ↑m 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆))
69	66, 68	imbitrrid 246	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ (∪ 𝑆 ↑m 𝑋)))
70	69	ssrdv 4001	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
71	70	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
72		elsni 4648	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} → 𝑥 = (∪ 𝑆 ↑m 𝑋))
73	72	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → 𝑥 = (∪ 𝑆 ↑m 𝑋))
74	71, 73	sseqtrrd 4037	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75		sseqin2 4231	. . . . . . . . . 10 ⊢ ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
76	74, 75	sylib 218	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77		eqid 2735	. . . . . . . . . . . 12 ⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
78	77	xkouni 23623	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
79		eqid 2735	. . . . . . . . . . . . 13 ⊢ ∪ (𝑆 ↑ko 𝑅) = ∪ (𝑆 ↑ko 𝑅)
80	79	topopn 22928	. . . . . . . . . . . 12 ⊢ ((𝑆 ↑ko 𝑅) ∈ Top → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
81	55, 80	syl 17	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
82	78, 81	eqeltrd 2839	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
83	82	adantr 480	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
84	76, 83	eqeltrd 2839	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
85		eqid 2735	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
86	85	rnmpo 7566	. . . . . . . . . 10 ⊢ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)}
87	86	eqabri 2883	. . . . . . . . 9 ⊢ (𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
88		cnvresima 6252	. . . . . . . . . . . . . . 15 ⊢ (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
89	70	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
90	89	resmptd 6060	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
91	90	cnveqd 5889	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = ◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
92	91	imaeq1d 6079	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
93	88, 92	eqtr3id 2789	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
94		fvex 6920	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤‘𝑘) ∈ V
95	94	rgenw 3063	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V
96		eqid 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))
97	96	fnmpt 6709	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
98	95, 97	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
99		elpreima 7078	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
101		fveq1 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
102		fvex 6920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑘) ∈ V
103	101, 96, 102	fvmpt 7016	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
104	103	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
105	104	eleq1d 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓‘𝑘) ∈ 𝑢))
106	102	snss 4790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑘) ∈ 𝑢 ↔ {(𝑓‘𝑘)} ⊆ 𝑢)
107	89	sselda 3995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ (∪ 𝑆 ↑m 𝑋))
108		elmapi 8888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ (∪ 𝑆 ↑m 𝑋) → 𝑓:𝑋⟶∪ 𝑆)
109		ffn 6737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋⟶∪ 𝑆 → 𝑓 Fn 𝑋)
110	107, 108, 109	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111		simplrl 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘 ∈ 𝑋)
112		fnsnfv 6988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 Fn 𝑋 ∧ 𝑘 ∈ 𝑋) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘}))
113	110, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘}))
114	113	sseq1d 4027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓‘𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
115	106, 114	bitrid 283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓‘𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
116	105, 115	bitrd 279	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
117	116	pm5.32da 579	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
118	100, 117	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
119	118	eqabdv 2873	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120		df-rab 3434	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121	119, 120	eqtr4di 2793	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
122	93, 121	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
123		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ Top)
124	11	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑆 ∈ Top)
125		simprl 771	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑘 ∈ 𝑋)
126	125	snssd 4814	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑘} ⊆ 𝑋)
127	2	toptopon 22939	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128	123, 127	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129		restsn2 23195	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
130	128, 125, 129	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
131		snfi 9082	. . . . . . . . . . . . . . . 16 ⊢ {𝑘} ∈ Fin
132		discmp 23422	. . . . . . . . . . . . . . . 16 ⊢ ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133	131, 132	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ 𝒫 {𝑘} ∈ Comp
134	130, 133	eqeltrdi 2847	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) ∈ Comp)
135		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
136	2, 123, 124, 126, 134, 135	xkoopn 23613	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆 ↑ko 𝑅))
137	122, 136	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138		ineq1 4221	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139	138	eleq1d 2824	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅) ↔ ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
140	137, 139	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
141	140	rexlimdvva 3211	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
142	141	imp 406	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
143	87, 142	sylan2b 594	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
144	84, 143	jaodan 959	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
145	65, 144	sylan2b 594	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
146	145	fmpttd 7135	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))⟶(𝑆 ↑ko 𝑅))
147	146	frnd 6745	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆 ↑ko 𝑅))
148	64, 147	eqsstrd 4034	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅))
149		tgfiss 23014	. . 3 ⊢ (((𝑆 ↑ko 𝑅) ∈ Top ∧ (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅)) → (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ↑ko 𝑅))
150	55, 148, 149	syl2anc 584	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ↑ko 𝑅))
151	54, 150	eqsstrd 4034	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537  ∃wex 1776   ∈ wcel 2106  {cab 2712  ∀wral 3059  ∃wrex 3068  {crab 3433  Vcvv 3478   ∖ cdif 3960   ∪ cun 3961   ∩ cin 3962   ⊆ wss 3963  𝒫 cpw 4605  {csn 4631  ∪ cuni 4912   ↦ cmpt 5231   × cxp 5687  ^◡ccnv 5688  ran crn 5690   ↾ cres 5691   “ cima 5692   Fn wfn 6558  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431   ∈ cmpo 7433   ↑_m cmap 8865  Xcixp 8936  Fincfn 8984  ficfi 9448   ↾_t crest 17467  topGenctg 17484  ∏_tcpt 17485  Topctop 22915  TopOnctopon 22932   Cn ccn 23248  Compccmp 23410   ↑_ko cxko 23585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-1o 8505  df-2o 8506  df-map 8867  df-ixp 8937  df-en 8985  df-dom 8986  df-fin 8988  df-fi 9449  df-rest 17469  df-topgen 17490  df-pt 17491  df-top 22916  df-topon 22933  df-bases 22969  df-cn 23251  df-cmp 23411  df-xko 23587

This theorem is referenced by:  xkopt  23679  xkopjcn  23680