Theorem xkopt 21268

Description: The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)

Assertion

Ref	Expression
xkopt	⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))

Proof of Theorem xkopt

Dummy variables 𝑓 𝑘 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		distop 20610	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)
2	1	adantl 481	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝒫 𝐴 ∈ Top)
3		simpl 472	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 ∈ Top)
4		unipw 4845	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
5	4	eqcomi 2619	. . . . 5 ⊢ 𝐴 = ∪ 𝒫 𝐴
6		eqid 2610	. . . . 5 ⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}
7		eqid 2610	. . . . 5 ⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
8	5, 6, 7	xkoval 21200	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ^ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
9	2, 3, 8	syl2anc 691	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
10		simpr 476	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
11		fconst6g 6007	. . . . . 6 ⊢ (𝑅 ∈ Top → (𝐴 × {𝑅}):𝐴⟶Top)
12	11	adantr 480	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 × {𝑅}):𝐴⟶Top)
13		pttop 21195	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝑅}):𝐴⟶Top) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
14	10, 12, 13	syl2anc 691	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
15		elpwi 4117	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
16		restdis 20792	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
17	15, 16	sylan2 490	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
18	17	adantll 746	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
19	18	eleq1d 2672	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp))
20		discmp 21011	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Comp)
21	19, 20	syl6bbr 277	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝑥 ∈ Fin))
22	21	rabbidva 3163	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin})
23		dfin5 3548	. . . . . . . . 9 ⊢ (𝒫 𝐴 ∩ Fin) = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin}
24	22, 23	syl6eqr 2662	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = (𝒫 𝐴 ∩ Fin))
25		eqidd 2611	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑅)
26		eqid 2610	. . . . . . . . . . 11 ⊢ ∪ 𝑅 = ∪ 𝑅
27	26	toptopon 20548	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
28		cndis 20905	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘∪ 𝑅)) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑𝑚 𝐴))
29	28	ancoms 468	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑𝑚 𝐴))
30	27, 29	sylanb 488	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑𝑚 𝐴))
31		rabeq 3166	. . . . . . . . 9 ⊢ ((𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑𝑚 𝐴) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
32	30, 31	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
33	24, 25, 32	mpt2eq123dv 6615	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
34	33	rneqd 5274	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
35		eqid 2610	. . . . . . 7 ⊢ (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
36	35	rnmpt2 6668	. . . . . 6 ⊢ ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}
37	34, 36	syl6eq 2660	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}})
38		elmapi 7765	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) → 𝑓:𝐴⟶∪ 𝑅)
39		eleq2 2677	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ 𝑣 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
40	39	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
41	40	bibi1d 332	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
42		eleq2 2677	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ ∪ 𝑅 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
43	42	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
44	43	bibi1d 332	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
45		inss1 3795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
46		simprl 790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ (𝒫 𝐴 ∩ Fin))
47	45, 46	sseldi 3566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ 𝒫 𝐴)
48	47	elpwid 4118	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ⊆ 𝐴)
49	48	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ 𝐴)
50	49	sselda 3568	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
51		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑘)
52	50, 51	2thd 254	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝑘))
53	52	imbi1d 330	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
54		ffvelrn 6265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝐴⟶∪ 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ∪ 𝑅)
55	54	ex 449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝐴⟶∪ 𝑅 → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
56	55	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
57	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
58		pm2.21 119	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 ∈ 𝑘 → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
59	58	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
60	57, 59	2thd 254	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
61	41, 44, 53, 60	ifbothda 4073	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
62	61	ralbidv2 2967	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
63		ffn 5958	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶∪ 𝑅 → 𝑓 Fn 𝐴)
64	63	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑓 Fn 𝐴)
65		vex 3176	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
66	65	elixp 7801	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
67	66	baib 942	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝐴 → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
68	64, 67	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
69		ffun 5961	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶∪ 𝑅 → Fun 𝑓)
70	69	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → Fun 𝑓)
71		fdm 5964	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴⟶∪ 𝑅 → dom 𝑓 = 𝐴)
72	71	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → dom 𝑓 = 𝐴)
73	49, 72	sseqtr4d 3605	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ dom 𝑓)
74		funimass4 6157	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝑓 ∧ 𝑘 ⊆ dom 𝑓) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
75	70, 73, 74	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
76	62, 68, 75	3bitr4d 299	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
77	38, 76	sylan2 490	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴)) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
78	77	rabbi2dva 3783	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑𝑚 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
79		elssuni 4403	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ 𝑅 → 𝑣 ⊆ ∪ 𝑅)
80	79	ad2antll 761	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑣 ⊆ ∪ 𝑅)
81		ssid 3587	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 ⊆ ∪ 𝑅
82		sseq1 3589	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (𝑣 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
83		sseq1 3589	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (∪ 𝑅 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
84	82, 83	ifboth 4074	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ ∪ 𝑅 ∧ ∪ 𝑅 ⊆ ∪ 𝑅) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
85	80, 81, 84	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
86	85	ralrimivw 2950	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
87		ss2ixp 7807	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅 → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
88	86, 87	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
89		simplr 788	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝐴 ∈ 𝑉)
90		uniexg 6853	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ V)
91	90	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∪ 𝑅 ∈ V)
92		ixpconstg 7803	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑅 ∈ V) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑𝑚 𝐴))
93	89, 91, 92	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑𝑚 𝐴))
94	88, 93	sseqtrd 3604	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑𝑚 𝐴))
95		sseqin2 3779	. . . . . . . . . . 11 ⊢ (X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑𝑚 𝐴) ↔ ((∪ 𝑅 ↑𝑚 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
96	94, 95	sylib 207	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑𝑚 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
97	78, 96	eqtr3d 2646	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
98	11	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝐴 × {𝑅}):𝐴⟶Top)
99		inss2 3796	. . . . . . . . . . 11 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ Fin
100	99, 46	sseldi 3566	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ Fin)
101		simplrr 797	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → 𝑣 ∈ 𝑅)
102	26	topopn 20536	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅)
103	102	ad3antrrr 762	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ∪ 𝑅 ∈ 𝑅)
104	101, 103	ifcld 4081	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ 𝑅)
105		simpll 786	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑅 ∈ Top)
106		fvconst2g 6372	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
107	105, 106	sylan 487	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
108	104, 107	eleqtrrd 2691	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ ((𝐴 × {𝑅})‘𝑥))
109		eldifn 3695	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → ¬ 𝑥 ∈ 𝑘)
110	109	iffalsed 4047	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
111	110	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
112		eldifi 3694	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → 𝑥 ∈ 𝐴)
113	112, 107	sylan2 490	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
114	113	unieqd 4382	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ∪ ((𝐴 × {𝑅})‘𝑥) = ∪ 𝑅)
115	111, 114	eqtr4d 2647	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ ((𝐴 × {𝑅})‘𝑥))
116	89, 98, 100, 108, 115	ptopn 21196	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ (∏t‘(𝐴 × {𝑅})))
117	97, 116	eqeltrd 2688	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅})))
118		eleq1 2676	. . . . . . . 8 ⊢ (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (𝑥 ∈ (∏t‘(𝐴 × {𝑅})) ↔ {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅}))))
119	117, 118	syl5ibrcom 236	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
120	119	rexlimdvva 3020	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
121	120	abssdv 3639	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ⊆ (∏t‘(𝐴 × {𝑅})))
122	37, 121	eqsstrd 3602	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅})))
123		tgfiss 20606	. . . 4 ⊢ (((∏t‘(𝐴 × {𝑅})) ∈ Top ∧ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
124	14, 122, 123	syl2anc 691	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
125	9, 124	eqsstrd 3602	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) ⊆ (∏t‘(𝐴 × {𝑅})))
126		eqid 2610	. . . . . . . 8 ⊢ (∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅}))
127	126, 26	ptuniconst 21211	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (∪ 𝑅 ↑𝑚 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
128	127	ancoms 468	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∪ 𝑅 ↑𝑚 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
129	30, 128	eqtrd 2644	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = ∪ (∏t‘(𝐴 × {𝑅})))
130	129	oveq2d 6565	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))))
131		eqid 2610	. . . . . 6 ⊢ ∪ (∏t‘(𝐴 × {𝑅})) = ∪ (∏t‘(𝐴 × {𝑅}))
132	131	restid 15917	. . . . 5 ⊢ ((∏t‘(𝐴 × {𝑅})) ∈ Top → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
133	14, 132	syl 17	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
134	130, 133	eqtrd 2644	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = (∏t‘(𝐴 × {𝑅})))
135	5, 126	xkoptsub 21267	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ^ko 𝒫 𝐴))
136	2, 3, 135	syl2anc 691	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ^ko 𝒫 𝐴))
137	134, 136	eqsstr3d 3603	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ⊆ (𝑅 ^ko 𝒫 𝐴))
138	125, 137	eqssd 3585	1 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ifcif 4036  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   × cxp 5036  dom cdm 5038  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑_𝑚 cmap 7744  Xcixp 7794  Fincfn 7841  ficfi 8199   ↾_t crest 15904  topGenctg 15921  ∏_tcpt 15922  Topctop 20517  TopOnctopon 20518   Cn ccn 20838  Compccmp 20999   ^_ko cxko 21174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-pt 15928  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841  df-cmp 21000  df-xko 21176

This theorem is referenced by:  tmdgsum  21709  tmdgsum2  21710  symgtgp  21715