Theorem xkoptsub 23973

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 23224	. . . . . . . 8 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
4	3	adantr 486	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋 ∈ 𝑅)
5		fconstg 6769	. . . . . . . . 9 ⊢ (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
6	5	adantl 487	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
7	6	ffnd 6710	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8		eqid 2761	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}
9	8	ptval 23889	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}))
10	4, 7, 9	syl2anc 596	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}))
11		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
12	11	snssd 4747	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
13	6, 12	fssd 6727	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14		eqid 2761	. . . . . . . . . 10 ⊢ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)
15	8, 14	ptbasfi 23900	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))))
16	4, 13, 15	syl2anc 596	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))))
17		fvconst2g 7208	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
18	17	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
19	18	unieqd 4880	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ∪ ((𝑋 × {𝑆})‘𝑛) = ∪ 𝑆)
20	19	ixpeq2dva 8940	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ 𝑆)
21		eqid 2761	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑆 = ∪ 𝑆
22	21	topopn 23224	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆)
23		ixpconstg 8934	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
24	3, 22, 23	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
25	20, 24	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
26	25	sneqd 4596	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} = {(∪ 𝑆 ↑m 𝑋)})
27		eqid 2761	. . . . . . . . . . . 12 ⊢ 𝑋 = 𝑋
28		fvconst2g 7208	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
29	28	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
30	25	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
31	30	mpteq1d 5195	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
32	31	cnveqd 5853	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
33	32	imaeq1d 6051	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
34	33	ralrimivw 3159	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
35	29, 34	jca 521	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
36	35	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
37		mpoeq123 7492	. . . . . . . . . . . 12 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
38	27, 36, 37	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
39	38	rneqd 5920	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
40	26, 39	uneq12d 4116	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))) = ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
41	40	fveq2d 6889	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))) = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
42	16, 41	eqtrd 2796	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
43	42	fveq2d 6889	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
44	10, 43	eqtrd 2796	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
45	1, 44	eqtrid 2808	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
46	45	oveq1d 7435	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47		firest 17603	. . . . 5 ⊢ (fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
48	47	fveq2i 6888	. . . 4 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49		fvex 6898	. . . . 5 ⊢ (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V
50		ovex 7453	. . . . 5 ⊢ (𝑅 Cn 𝑆) ∈ V
51		tgrest 23477	. . . . 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 705	. . . 4 ⊢ (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
53	48, 52	eqtri 2784	. . 3 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
54	46, 53	eqtr4di 2814	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55		xkotop 23907	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
56		snex 5397	. . . . . 6 ⊢ {(∪ 𝑆 ↑m 𝑋)} ∈ V
57		mpoexga 8090	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
58	3, 57	sylan 592	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
59		rnexg 7914	. . . . . . 7 ⊢ ((𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
60	58, 59	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
61		unexg 7760	. . . . . 6 ⊢ (({(∪ 𝑆 ↑m 𝑋)} ∈ V ∧ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
62	56, 60, 61	sylancr 599	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
63		restval 17597	. . . . 5 ⊢ ((({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
64	62, 50, 63	sylancl 598	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
65		elun 4100	. . . . . . 7 ⊢ (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
66	2, 21	cnf 23564	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋⟶∪ 𝑆)
67		elmapg 8859	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅) → (𝑥 ∈ (∪ 𝑆 ↑m 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆))
68	22, 3, 67	syl2anr 609	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (∪ 𝑆 ↑m 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆))
69	66, 68	imbitrrid 249	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ (∪ 𝑆 ↑m 𝑋)))
70	69	ssrdv 3937	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
71	70	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
72		elsni 4601	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} → 𝑥 = (∪ 𝑆 ↑m 𝑋))
73	72	adantl 487	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → 𝑥 = (∪ 𝑆 ↑m 𝑋))
74	71, 73	sseqtrrd 3968	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75		sseqin2 4169	. . . . . . . . . 10 ⊢ ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
76	74, 75	sylib 221	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
78	77	xkouni 23918	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
79		eqid 2761	. . . . . . . . . . . . 13 ⊢ ∪ (𝑆 ↑ko 𝑅) = ∪ (𝑆 ↑ko 𝑅)
80	79	topopn 23224	. . . . . . . . . . . 12 ⊢ ((𝑆 ↑ko 𝑅) ∈ Top → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
81	55, 80	syl 18	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
82	78, 81	eqeltrd 2861	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
83	82	adantr 486	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
84	76, 83	eqeltrd 2861	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
85		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
86	85	rnmpo 7553	. . . . . . . . . 10 ⊢ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)}
87	86	eqabri 2903	. . . . . . . . 9 ⊢ (𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
88		cnvresima 6231	. . . . . . . . . . . . . . 15 ⊢ (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
89	70	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
90	89	resmptd 6032	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
91	90	cnveqd 5853	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = ◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
92	91	imaeq1d 6051	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
93	88, 92	eqtr3id 2810	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
94		fvex 6898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤‘𝑘) ∈ V
95	94	rgenw 3081	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V
96		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))
97	96	fnmpt 6679	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
98	95, 97	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
99		elpreima 7057	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
100	98, 99	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
101		fveq1 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
102		fvex 6898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑘) ∈ V
103	101, 96, 102	fvmpt 6993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
104	103	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
105	104	eleq1d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓‘𝑘) ∈ 𝑢))
106	102	snss 4745	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑘) ∈ 𝑢 ↔ {(𝑓‘𝑘)} ⊆ 𝑢)
107	89	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ (∪ 𝑆 ↑m 𝑋))
108		elmapi 8869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ (∪ 𝑆 ↑m 𝑋) → 𝑓:𝑋⟶∪ 𝑆)
109		ffn 6709	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋⟶∪ 𝑆 → 𝑓 Fn 𝑋)
110	107, 108, 109	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111		simplrl 789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘 ∈ 𝑋)
112		fnsnfv 6964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 Fn 𝑋 ∧ 𝑘 ∈ 𝑋) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘}))
113	110, 111, 112	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘}))
114	113	sseq1d 3962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓‘𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
115	106, 114	bitrid 286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓‘𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
116	105, 115	bitrd 282	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
117	116	pm5.32da 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
118	100, 117	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
119	118	eqabdv 2894	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120		df-rab 3414	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121	119, 120	eqtr4di 2814	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
122	93, 121	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
123		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ Top)
124	11	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑆 ∈ Top)
125		simprl 783	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑘 ∈ 𝑋)
126	125	snssd 4747	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑘} ⊆ 𝑋)
127	2	toptopon 23235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128	123, 127	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129		restsn2 23489	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
130	128, 125, 129	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
131		snfi 9071	. . . . . . . . . . . . . . . 16 ⊢ {𝑘} ∈ Fin
132		discmp 23716	. . . . . . . . . . . . . . . 16 ⊢ ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133	131, 132	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ 𝒫 {𝑘} ∈ Comp
134	130, 133	eqeltrdi 2869	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) ∈ Comp)
135		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
136	2, 123, 124, 126, 134, 135	xkoopn 23908	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆 ↑ko 𝑅))
137	122, 136	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138		ineq1 4159	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139	138	eleq1d 2846	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅) ↔ ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
140	137, 139	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
141	140	rexlimdvva 3220	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
142	141	imp 412	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
143	87, 142	sylan2b 606	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
144	84, 143	jaodan 972	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
145	65, 144	sylan2b 606	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
146	145	fmpttd 7115	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))⟶(𝑆 ↑ko 𝑅))
147	146	frnd 6718	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆 ↑ko 𝑅))
148	64, 147	eqsstrd 3965	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅))
149		tgfiss 23309	. . 3 ⊢ (((𝑆 ↑ko 𝑅) ∈ Top ∧ (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅)) → (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ↑ko 𝑅))
150	55, 148, 149	syl2anc 596	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ↑ko 𝑅))
151	54, 150	eqsstrd 3965	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867   ↦ cmpt 5186   × cxp 5649  ^◡ccnv 5650  ran crn 5652   ↾ cres 5653   “ cima 5654   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422   ↑_m cmap 8847  Xcixp 8925  Fincfn 8973  ficfi 9402   ↾_t crest 17591  topGenctg 17608  ∏_tcpt 17609  Topctop 23211  TopOnctopon 23228   Cn ccn 23542  Compccmp 23704   ↑_ko cxko 23880

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-1o 8476  df-2o 8477  df-map 8849  df-ixp 8926  df-en 8974  df-dom 8975  df-fin 8977  df-fi 9403  df-rest 17593  df-topgen 17614  df-pt 17615  df-top 23212  df-topon 23229  df-bases 23264  df-cn 23545  df-cmp 23705  df-xko 23882

This theorem is used by:  xkopt  23974  xkopjcn  23975