Theorem xkoptsub 23619

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 22871	. . . . . . . 8 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
4	3	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋 ∈ 𝑅)
5		fconstg 6727	. . . . . . . . 9 ⊢ (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
6	5	adantl 481	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
7	6	ffnd 6669	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8		eqid 2736	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}
9	8	ptval 23535	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}))
10	4, 7, 9	syl2anc 585	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}))
11		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
12	11	snssd 4730	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
13	6, 12	fssd 6685	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14		eqid 2736	. . . . . . . . . 10 ⊢ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)
15	8, 14	ptbasfi 23546	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))))
16	4, 13, 15	syl2anc 585	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))))
17		fvconst2g 7157	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
18	17	adantll 715	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
19	18	unieqd 4863	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ∪ ((𝑋 × {𝑆})‘𝑛) = ∪ 𝑆)
20	19	ixpeq2dva 8860	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = X𝑛 ∈ 𝑋 ∪ 𝑆)
21		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑆 = ∪ 𝑆
22	21	topopn 22871	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆)
23		ixpconstg 8854	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
24	3, 22, 23	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪ 𝑆 ↑m 𝑋))
25	20, 24	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
26	25	sneqd 4579	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} = {(∪ 𝑆 ↑m 𝑋)})
27		eqid 2736	. . . . . . . . . . . 12 ⊢ 𝑋 = 𝑋
28		fvconst2g 7157	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
29	28	adantll 715	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
30	25	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑m 𝑋))
31	30	mpteq1d 5175	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
32	31	cnveqd 5830	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)))
33	32	imaeq1d 6024	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
34	33	ralrimivw 3133	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
35	29, 34	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
36	35	ralrimiva 3129	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
37		mpoeq123 7439	. . . . . . . . . . . 12 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
38	27, 36, 37	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
39	38	rneqd 5893	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))
40	26, 39	uneq12d 4109	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))) = ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
41	40	fveq2d 6844	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))) = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
42	16, 41	eqtrd 2771	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))
43	42	fveq2d 6844	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
44	10, 43	eqtrd 2771	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
45	1, 44	eqtrid 2783	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))))
46	45	oveq1d 7382	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47		firest 17395	. . . . 5 ⊢ (fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
48	47	fveq2i 6843	. . . 4 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49		fvex 6853	. . . . 5 ⊢ (fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V
50		ovex 7400	. . . . 5 ⊢ (𝑅 Cn 𝑆) ∈ V
51		tgrest 23124	. . . . 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 693	. . . 4 ⊢ (topGen‘((fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
53	48, 52	eqtri 2759	. . 3 ⊢ (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
54	46, 53	eqtr4di 2789	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55		xkotop 23553	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
56		snex 5381	. . . . . 6 ⊢ {(∪ 𝑆 ↑m 𝑋)} ∈ V
57		mpoexga 8030	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
58	3, 57	sylan 581	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
59		rnexg 7853	. . . . . . 7 ⊢ ((𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
60	58, 59	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
61		unexg 7697	. . . . . 6 ⊢ (({(∪ 𝑆 ↑m 𝑋)} ∈ V ∧ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
62	56, 60, 61	sylancr 588	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
63		restval 17389	. . . . 5 ⊢ ((({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
64	62, 50, 63	sylancl 587	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
65		elun 4093	. . . . . . 7 ⊢ (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))
66	2, 21	cnf 23211	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋⟶∪ 𝑆)
67		elmapg 8786	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅) → (𝑥 ∈ (∪ 𝑆 ↑m 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆))
68	22, 3, 67	syl2anr 598	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (∪ 𝑆 ↑m 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆))
69	66, 68	imbitrrid 246	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ (∪ 𝑆 ↑m 𝑋)))
70	69	ssrdv 3927	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
71	70	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
72		elsni 4584	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} → 𝑥 = (∪ 𝑆 ↑m 𝑋))
73	72	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → 𝑥 = (∪ 𝑆 ↑m 𝑋))
74	71, 73	sseqtrrd 3959	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75		sseqin2 4163	. . . . . . . . . 10 ⊢ ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
76	74, 75	sylib 218	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
78	77	xkouni 23564	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
79		eqid 2736	. . . . . . . . . . . . 13 ⊢ ∪ (𝑆 ↑ko 𝑅) = ∪ (𝑆 ↑ko 𝑅)
80	79	topopn 22871	. . . . . . . . . . . 12 ⊢ ((𝑆 ↑ko 𝑅) ∈ Top → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
81	55, 80	syl 17	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ (𝑆 ↑ko 𝑅) ∈ (𝑆 ↑ko 𝑅))
82	78, 81	eqeltrd 2836	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
83	82	adantr 480	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆 ↑ko 𝑅))
84	76, 83	eqeltrd 2836	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
85		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
86	85	rnmpo 7500	. . . . . . . . . 10 ⊢ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)}
87	86	eqabri 2878	. . . . . . . . 9 ⊢ (𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))
88		cnvresima 6194	. . . . . . . . . . . . . . 15 ⊢ (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
89	70	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 Cn 𝑆) ⊆ (∪ 𝑆 ↑m 𝑋))
90	89	resmptd 6005	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
91	90	cnveqd 5830	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = ◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)))
92	91	imaeq1d 6024	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡((𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
93	88, 92	eqtr3id 2785	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢))
94		fvex 6853	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤‘𝑘) ∈ V
95	94	rgenw 3055	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V
96		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))
97	96	fnmpt 6638	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
98	95, 97	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆))
99		elpreima 7010	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢)))
101		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
102		fvex 6853	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑘) ∈ V
103	101, 96, 102	fvmpt 6947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
104	103	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘))
105	104	eleq1d 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓‘𝑘) ∈ 𝑢))
106	102	snss 4728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑘) ∈ 𝑢 ↔ {(𝑓‘𝑘)} ⊆ 𝑢)
107	89	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ (∪ 𝑆 ↑m 𝑋))
108		elmapi 8796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ (∪ 𝑆 ↑m 𝑋) → 𝑓:𝑋⟶∪ 𝑆)
109		ffn 6668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋⟶∪ 𝑆 → 𝑓 Fn 𝑋)
110	107, 108, 109	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111		simplrl 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘 ∈ 𝑋)
112		fnsnfv 6919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 Fn 𝑋 ∧ 𝑘 ∈ 𝑋) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘}))
113	110, 111, 112	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘}))
114	113	sseq1d 3953	. . . . . . . . . . . . . . . . . . . 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 2869	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120		df-rab 3390	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121	119, 120	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
122	93, 121	eqtrd 2771	. . . . . . . . . . . . 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 4730	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑘} ⊆ 𝑋)
127	2	toptopon 22882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128	123, 127	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129		restsn2 23136	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
130	128, 125, 129	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘})
131		snfi 8990	. . . . . . . . . . . . . . . 16 ⊢ {𝑘} ∈ Fin
132		discmp 23363	. . . . . . . . . . . . . . . 16 ⊢ ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133	131, 132	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ 𝒫 {𝑘} ∈ Comp
134	130, 133	eqeltrdi 2844	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) ∈ Comp)
135		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆)
136	2, 123, 124, 126, 134, 135	xkoopn 23554	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆 ↑ko 𝑅))
137	122, 136	eqeltrd 2836	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
138		ineq1 4153	. . . . . . . . . . . . 13 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139	138	eleq1d 2821	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅) ↔ ((◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
140	137, 139	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
141	140	rexlimdvva 3194	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅)))
142	141	imp 406	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
143	87, 142	sylan2b 595	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
144	84, 143	jaodan 960	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {(∪ 𝑆 ↑m 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
145	65, 144	sylan2b 595	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ↑ko 𝑅))
146	145	fmpttd 7067	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))⟶(𝑆 ↑ko 𝑅))
147	146	frnd 6676	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆 ↑ko 𝑅))
148	64, 147	eqsstrd 3956	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅))
149		tgfiss 22956	. . 3 ⊢ (((𝑆 ↑ko 𝑅) ∈ Top ∧ (({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅)) → (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ↑ko 𝑅))
150	55, 148, 149	syl2anc 585	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘(fi‘(({(∪ 𝑆 ↑m 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑m 𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ↑ko 𝑅))
151	54, 150	eqsstrd 3956	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2714  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ∩ cin 3888   ⊆ wss 3889  𝒫 cpw 4541  {csn 4567  ∪ cuni 4850   ↦ cmpt 5166   × cxp 5629  ^◡ccnv 5630  ran crn 5632   ↾ cres 5633   “ cima 5634   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369   ↑_m cmap 8773  Xcixp 8845  Fincfn 8893  ficfi 9323   ↾_t crest 17383  topGenctg 17400  ∏_tcpt 17401  Topctop 22858  TopOnctopon 22875   Cn ccn 23189  Compccmp 23351   ↑_ko cxko 23526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-1o 8405  df-2o 8406  df-map 8775  df-ixp 8846  df-en 8894  df-dom 8895  df-fin 8897  df-fi 9324  df-rest 17385  df-topgen 17406  df-pt 17407  df-top 22859  df-topon 22876  df-bases 22911  df-cn 23192  df-cmp 23352  df-xko 23528

This theorem is referenced by:  xkopt  23620  xkopjcn  23621