Theorem xkoptsub 23881

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 23132	. . . . . . . 8 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
4	3	adantr 486	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋 ∈ 𝑅)
5		fconstg 6763	. . . . . . . . 9 ⊢ (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
6	5	adantl 487	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
7	6	ffnd 6704	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8		eqid 2760	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}
9	8	ptval 23797	. . . . . . 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 6721	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14		eqid 2760	. . . . . . . . . 10 ⊢ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)
15	8, 14	ptbasfi 23808	. . . . . . . . 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 7202	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
18	17	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
19	18	unieqd 4880	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ∪ ((𝑋 × {𝑆})‘𝑛) = ∪ 𝑆)
20	19	ixpeq2dva 8920	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ 𝑆)
21		eqid 2760	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑆 = ∪ 𝑆
22	21	topopn 23132	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆)
23		ixpconstg 8914	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
24	3, 22, 23	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
25	20, 24	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
26	25	sneqd 4596	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} = {(∪ 𝑆 ↑m 𝑋)})
27		eqid 2760	. . . . . . . . . . . 12 ⊢ 𝑋 = 𝑋
28		fvconst2g 7202	. . . . . . . . . . . . . . 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 5855	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
33	32	imaeq1d 6055	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
34	33	ralrimivw 3158	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
35	29, 34	jca 521	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
36	35	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
37		mpoeq123 7486	. . . . . . . . . . . 12 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
38	27, 36, 37	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
39	38	rneqd 5922	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
40	26, 39	uneq12d 4116	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))) = ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
41	40	fveq2d 6883	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))) = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
42	16, 41	eqtrd 2795	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
43	42	fveq2d 6883	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
44	10, 43	eqtrd 2795	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
45	1, 44	eqtrid 2807	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
46	45	oveq1d 7429	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47		firest 17518	. . . . 5 ⊢ (fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
48	47	fveq2i 6882	. . . 4 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49		fvex 6892	. . . . 5 ⊢ (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V
50		ovex 7447	. . . . 5 ⊢ (𝑅 Cn 𝑆) ∈ V
51		tgrest 23385	. . . . 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 2783	. . 3 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
54	46, 53	eqtr4di 2813	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55		xkotop 23815	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
56		snex 5404	. . . . . 6 ⊢ {(∪ 𝑆 ↑m 𝑋)} ∈ V
57		mpoexga 8077	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
58	3, 57	sylan 592	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
59		rnexg 7900	. . . . . . 7 ⊢ ((𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
60	58, 59	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
61		unexg 7746	. . . . . 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 17512	. . . . 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 23472	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋⟶∪ 𝑆)
67		elmapg 8839	. . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . 12 ⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
78	77	xkouni 23826	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
79		eqid 2760	. . . . . . . . . . . . 13 ⊢ ∪ (𝑆 ↑ko 𝑅) = ∪ (𝑆 ↑ko 𝑅)
80	79	topopn 23132	. . . . . . . . . . . 12 ⊢ ((𝑆 ↑ko 𝑅) ∈ Top → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
81	55, 80	syl 18	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
82	78, 81	eqeltrd 2860	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
83	82	adantr 486	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
84	76, 83	eqeltrd 2860	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
85		eqid 2760	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
86	85	rnmpo 7547	. . . . . . . . . 10 ⊢ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)}
87	86	eqabri 2902	. . . . . . . . 9 ⊢ (𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
88		cnvresima 6226	. . . . . . . . . . . . . . 15 ⊢ (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
89	70	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
90	89	resmptd 6036	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
91	90	cnveqd 5855	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = ◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
92	91	imaeq1d 6055	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
93	88, 92	eqtr3id 2809	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
94		fvex 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤‘𝑘) ∈ V
95	94	rgenw 3080	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V
96		eqid 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))
97	96	fnmpt 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
98	95, 97	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
99		elpreima 7051	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
100	98, 99	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
101		fveq1 6878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
102		fvex 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑘) ∈ V
103	101, 96, 102	fvmpt 6987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
104	103	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
105	104	eleq1d 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓‘𝑘) ∈ 𝑢))
106	102	snss 4745	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑘) ∈ 𝑢 ↔ {(𝑓‘𝑘)} ⊆ 𝑢)
107	89	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ (∪ 𝑆 ↑m 𝑋))
108		elmapi 8849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ (∪ 𝑆 ↑m 𝑋) → 𝑓:𝑋⟶∪ 𝑆)
109		ffn 6703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋⟶∪ 𝑆 → 𝑓 Fn 𝑋)
110	107, 108, 109	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111		simplrl 789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘 ∈ 𝑋)
112		fnsnfv 6958	. . . . . . . . . . . . . . . . . . . . . 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 2893	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120		df-rab 3413	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121	119, 120	eqtr4di 2813	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
122	93, 121	eqtrd 2795	. . . . . . . . . . . . 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 23143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128	123, 127	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129		restsn2 23397	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
130	128, 125, 129	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
131		snfi 9051	. . . . . . . . . . . . . . . 16 ⊢ {𝑘} ∈ Fin
132		discmp 23624	. . . . . . . . . . . . . . . 16 ⊢ ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133	131, 132	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ 𝒫 {𝑘} ∈ Comp
134	130, 133	eqeltrdi 2868	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) ∈ Comp)
135		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
136	2, 123, 124, 126, 134, 135	xkoopn 23816	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆 ↑ko 𝑅))
137	122, 136	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138		ineq1 4159	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139	138	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅) ↔ ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
140	137, 139	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
141	140	rexlimdvva 3219	. . . . . . . . . 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 7109	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))⟶(𝑆 ↑ko 𝑅))
147	146	frnd 6712	. . . 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 23217	. . 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 2738  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867   ↦ cmpt 5186   × cxp 5653  ^◡ccnv 5654  ran crn 5656   ↾ cres 5657   “ cima 5658   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7414   ∈ cmpo 7416   ↑_m cmap 8827  Xcixp 8905  Fincfn 8953  ficfi 9381   ↾_t crest 17506  topGenctg 17523  ∏_tcpt 17524  Topctop 23119  TopOnctopon 23136   Cn ccn 23450  Compccmp 23612   ↑_ko cxko 23788

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 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-1st 7987  df-2nd 7988  df-1o 8456  df-2o 8457  df-map 8829  df-ixp 8906  df-en 8954  df-dom 8955  df-fin 8957  df-fi 9382  df-rest 17508  df-topgen 17529  df-pt 17530  df-top 23120  df-topon 23137  df-bases 23172  df-cn 23453  df-cmp 23613  df-xko 23790

This theorem is used by:  xkopt  23882  xkopjcn  23883