xkococn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xkococn		Structured version Visualization version GIF version

Theorem xkococn 22262

Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)

**Hypothesis**
Ref	Expression
xkococn.1	⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))

**Assertion**
Ref	Expression
xkococn	⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝐹 ∈ (((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) Cn (𝑇 ↑_ko 𝑅)))

Distinct variable groups: 𝑓,𝑔,𝑅 𝑆,𝑓,𝑔 𝑇,𝑓,𝑔 Allowed substitution hints: 𝐹(𝑓,𝑔)

Proof of Theorem xkococn Dummy variables 𝑘 𝑎 𝑣 𝑥 𝑦 𝑧 𝑏 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprr 771	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑓 ∈ (𝑆 Cn 𝑇) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆))
2		simprl 769	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑓 ∈ (𝑆 Cn 𝑇) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 ∈ (𝑆 Cn 𝑇))
3		cnco 21868	. . . . 5 ⊢ ((𝑔 ∈ (𝑅 Cn 𝑆) ∧ 𝑓 ∈ (𝑆 Cn 𝑇)) → (𝑓 ∘ 𝑔) ∈ (𝑅 Cn 𝑇))
4	1, 2, 3	syl2anc 586	. . . 4 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑓 ∈ (𝑆 Cn 𝑇) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ∘ 𝑔) ∈ (𝑅 Cn 𝑇))
5	4	ralrimivva 3191	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → ∀𝑓 ∈ (𝑆 Cn 𝑇)∀𝑔 ∈ (𝑅 Cn 𝑆)(𝑓 ∘ 𝑔) ∈ (𝑅 Cn 𝑇))
6		xkococn.1	. . . 4 ⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
7	6	fmpo 7760	. . 3 ⊢ (∀𝑓 ∈ (𝑆 Cn 𝑇)∀𝑔 ∈ (𝑅 Cn 𝑆)(𝑓 ∘ 𝑔) ∈ (𝑅 Cn 𝑇) ↔ 𝐹:((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))⟶(𝑅 Cn 𝑇))
8	5, 7	sylib 220	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝐹:((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))⟶(𝑅 Cn 𝑇))
9		eqid 2821	. . . . . . 7 ⊢ (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})
10	9	rnmpo 7278	. . . . . 6 ⊢ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}}
11	10	eleq2i 2904	. . . . 5 ⊢ (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ↔ 𝑥 ∈ {𝑥 ∣ ∃𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}})
12		abid 2803	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}} ↔ ∃𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})
13		oveq2 7158	. . . . . . 7 ⊢ (𝑦 = 𝑘 → (𝑅 ↾_t 𝑦) = (𝑅 ↾_t 𝑘))
14	13	eleq1d 2897	. . . . . 6 ⊢ (𝑦 = 𝑘 → ((𝑅 ↾_t 𝑦) ∈ Comp ↔ (𝑅 ↾_t 𝑘) ∈ Comp))
15	14	rexrab 3686	. . . . 5 ⊢ (∃𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ ∃𝑘 ∈ 𝒫 ∪ 𝑅((𝑅 ↾_t 𝑘) ∈ Comp ∧ ∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))
16	11, 12, 15	3bitri 299	. . . 4 ⊢ (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ 𝒫 ∪ 𝑅((𝑅 ↾_t 𝑘) ∈ Comp ∧ ∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))
17	8	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → 𝐹:((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))⟶(𝑅 Cn 𝑇))
18		ffn 6508	. . . . . . . . . . . . 13 ⊢ (𝐹:((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))⟶(𝑅 Cn 𝑇) → 𝐹 Fn ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
19		elpreima 6822	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) → (𝑦 ∈ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ↔ (𝑦 ∈ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) ∧ (𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))
20	17, 18, 19	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → (𝑦 ∈ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ↔ (𝑦 ∈ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) ∧ (𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))
21		coeq1 5722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑎 → (𝑓 ∘ 𝑔) = (𝑎 ∘ 𝑔))
22		coeq2 5723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑏 → (𝑎 ∘ 𝑔) = (𝑎 ∘ 𝑏))
23		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑎 ∈ V
24		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑏 ∈ V
25	23, 24	coex 7629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∘ 𝑏) ∈ V
26	21, 22, 6, 25	ovmpo 7304	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) → (𝑎𝐹𝑏) = (𝑎 ∘ 𝑏))
27	26	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ (𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆))) → (𝑎𝐹𝑏) = (𝑎 ∘ 𝑏))
28	27	eleq1d 2897	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ (𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆))) → ((𝑎𝐹𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ (𝑎 ∘ 𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))
29		imaeq1 5918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = (𝑎 ∘ 𝑏) → (ℎ “ 𝑘) = ((𝑎 ∘ 𝑏) “ 𝑘))
30	29	sseq1d 3997	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = (𝑎 ∘ 𝑏) → ((ℎ “ 𝑘) ⊆ 𝑣 ↔ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣))
31	30	elrab 3679	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∘ 𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ ((𝑎 ∘ 𝑏) ∈ (𝑅 Cn 𝑇) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣))
32	31	simprbi 499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∘ 𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)
33		simp2 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝑆 ∈ 𝑛-Locally Comp)
34	33	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → 𝑆 ∈ 𝑛-Locally Comp)
35		elpwi 4550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝒫 ∪ 𝑅 → 𝑘 ⊆ ∪ 𝑅)
36	35	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) → 𝑘 ⊆ ∪ 𝑅)
37	36	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → 𝑘 ⊆ ∪ 𝑅)
38		simprr 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) → (𝑅 ↾_t 𝑘) ∈ Comp)
39	38	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → (𝑅 ↾_t 𝑘) ∈ Comp)
40		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → 𝑣 ∈ 𝑇)
41		simprll 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → 𝑎 ∈ (𝑆 Cn 𝑇))
42		simprlr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → 𝑏 ∈ (𝑅 Cn 𝑆))
43		simprr 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)
44	6, 34, 37, 39, 40, 41, 42, 43	xkococnlem 22261	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ ((𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆)) ∧ ((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))
45	44	expr 459	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ (𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆))) → (((𝑎 ∘ 𝑏) “ 𝑘) ⊆ 𝑣 → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
46	32, 45	syl5 34	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ (𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆))) → ((𝑎 ∘ 𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
47	28, 46	sylbid 242	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ (𝑎 ∈ (𝑆 Cn 𝑇) ∧ 𝑏 ∈ (𝑅 Cn 𝑆))) → ((𝑎𝐹𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
48	47	ralrimivva 3191	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → ∀𝑎 ∈ (𝑆 Cn 𝑇)∀𝑏 ∈ (𝑅 Cn 𝑆)((𝑎𝐹𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
49		fveq2 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝐹‘𝑦) = (𝐹‘⟨𝑎, 𝑏⟩))
50		df-ov 7153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎𝐹𝑏) = (𝐹‘⟨𝑎, 𝑏⟩)
51	49, 50	syl6eqr 2874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝐹‘𝑦) = (𝑎𝐹𝑏))
52	51	eleq1d 2897	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ (𝑎𝐹𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))
53		eleq1 2900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ 𝑧 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑧))
54	53	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
55	54	rexbidv 3297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})) ↔ ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
56	52, 55	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))) ↔ ((𝑎𝐹𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))))
57	56	ralxp 5706	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))((𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))) ↔ ∀𝑎 ∈ (𝑆 Cn 𝑇)∀𝑏 ∈ (𝑅 Cn 𝑆)((𝑎𝐹𝑏) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝑎, 𝑏⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
58	48, 57	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → ∀𝑦 ∈ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))((𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
59	58	r19.21bi 3208	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) ∧ 𝑦 ∈ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))) → ((𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
60	59	expimpd 456	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → ((𝑦 ∈ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)) ∧ (𝐹‘𝑦) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
61	20, 60	sylbid 242	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → (𝑦 ∈ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
62	61	ralrimiv 3181	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → ∀𝑦 ∈ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))
63		nllytop 22075	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
64	63	3ad2ant2 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝑆 ∈ Top)
65		simp3 1134	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝑇 ∈ Top)
66		xkotop 22190	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ Top)
67	64, 65, 66	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ Top)
68		simp1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝑅 ∈ Top)
69		xkotop 22190	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ Top)
70	68, 64, 69	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ Top)
71		txtop 22171	. . . . . . . . . . . . 13 ⊢ (((𝑇 ↑_ko 𝑆) ∈ Top ∧ (𝑆 ↑_ko 𝑅) ∈ Top) → ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∈ Top)
72	67, 70, 71	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∈ Top)
73	72	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∈ Top)
74		eltop2 21577	. . . . . . . . . . 11 ⊢ (((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∈ Top → ((^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ↔ ∀𝑦 ∈ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
75	73, 74	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → ((^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ↔ ∀𝑦 ∈ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
76	62, 75	mpbird 259	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
77		imaeq2 5919	. . . . . . . . . 10 ⊢ (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))
78	77	eleq1d 2897	. . . . . . . . 9 ⊢ (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ((^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ↔ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
79	76, 78	syl5ibrcom 249	. . . . . . . 8 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) ∧ 𝑣 ∈ 𝑇) → (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
80	79	rexlimdva 3284	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ (𝑘 ∈ 𝒫 ∪ 𝑅 ∧ (𝑅 ↾_t 𝑘) ∈ Comp)) → (∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
81	80	anassrs 470	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ 𝑘 ∈ 𝒫 ∪ 𝑅) ∧ (𝑅 ↾_t 𝑘) ∈ Comp) → (∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
82	81	expimpd 456	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) ∧ 𝑘 ∈ 𝒫 ∪ 𝑅) → (((𝑅 ↾_t 𝑘) ∈ Comp ∧ ∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → (^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
83	82	rexlimdva 3284	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (∃𝑘 ∈ 𝒫 ∪ 𝑅((𝑅 ↾_t 𝑘) ∈ Comp ∧ ∃𝑣 ∈ 𝑇 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → (^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
84	16, 83	syl5bi 244	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → (^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))))
85	84	ralrimiv 3181	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → ∀𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})(^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
86		eqid 2821	. . . . . 6 ⊢ (𝑇 ↑_ko 𝑆) = (𝑇 ↑_ko 𝑆)
87	86	xkotopon 22202	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ (TopOn‘(𝑆 Cn 𝑇)))
88	64, 65, 87	syl2anc 586	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ (TopOn‘(𝑆 Cn 𝑇)))
89		eqid 2821	. . . . . 6 ⊢ (𝑆 ↑_ko 𝑅) = (𝑆 ↑_ko 𝑅)
90	89	xkotopon 22202	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆)))
91	68, 64, 90	syl2anc 586	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆)))
92		txtopon 22193	. . . 4 ⊢ (((𝑇 ↑_ko 𝑆) ∈ (TopOn‘(𝑆 Cn 𝑇)) ∧ (𝑆 ↑_ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) → ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∈ (TopOn‘((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))))
93	88, 91, 92	syl2anc 586	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∈ (TopOn‘((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))))
94		ovex 7183	. . . . . 6 ⊢ (𝑅 Cn 𝑇) ∈ V
95	94	pwex 5273	. . . . 5 ⊢ 𝒫 (𝑅 Cn 𝑇) ∈ V
96		eqid 2821	. . . . . . 7 ⊢ ∪ 𝑅 = ∪ 𝑅
97		eqid 2821	. . . . . . 7 ⊢ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp} = {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}
98	96, 97, 9	xkotf 22187	. . . . . 6 ⊢ (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}):({𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp} × 𝑇)⟶𝒫 (𝑅 Cn 𝑇)
99		frn 6514	. . . . . 6 ⊢ ((𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}):({𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp} × 𝑇)⟶𝒫 (𝑅 Cn 𝑇) → ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑇))
100	98, 99	ax-mp 5	. . . . 5 ⊢ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑇)
101	95, 100	ssexi 5218	. . . 4 ⊢ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ V
102	101	a1i 11	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ V)
103	96, 97, 9	xkoval 22189	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
104	103	3adant2 1127	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}))))
105		eqid 2821	. . . . 5 ⊢ (𝑇 ↑_ko 𝑅) = (𝑇 ↑_ko 𝑅)
106	105	xkotopon 22202	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑇)))
107	106	3adant2 1127	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑇)))
108	93, 102, 104, 107	subbascn 21856	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → (𝐹 ∈ (((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) Cn (𝑇 ↑_ko 𝑅)) ↔ (𝐹:((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))⟶(𝑅 Cn 𝑇) ∧ ∀𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅 ∣ (𝑅 ↾_t 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})(^◡𝐹 “ 𝑥) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))))
109	8, 85, 108	mpbir2and 711	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝐹 ∈ (((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) Cn (𝑇 ↑_ko 𝑅)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 {cab 2799 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3494 ⊆ wss 3935 𝒫 cpw 4538 ⟨cop 4566 ∪ cuni 4831 × cxp 5547 ^◡ccnv 5548 ran crn 5550 “ cima 5552 ∘ ccom 5553 Fn wfn 6344 ⟶wf 6345 ‘cfv 6349 (class class class)co 7150 ∈ cmpo 7152 ficfi 8868 ↾_t crest 16688 topGenctg 16705 Topctop 21495 TopOnctopon 21512 Cn ccn 21826 Compccmp 21988 𝑛-Locally cnlly 22067 ×_t ctx 22162 ↑_ko cxko 22163

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 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-iin 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-fin 8507 df-fi 8869 df-rest 16690 df-topgen 16711 df-top 21496 df-topon 21513 df-bases 21548 df-ntr 21622 df-nei 21700 df-cn 21829 df-cmp 21989 df-nlly 22069 df-tx 22164 df-xko 22165

This theorem is referenced by: cnmptkk 22285 xkofvcn 22286 efmndtmd 22703

W3C validator