Theorem xkopt 23703

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 23043	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)
2		simpl 486	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 ∈ Top)
3		unipw 5414	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
4	3	eqcomi 2770	. . . . 5 ⊢ 𝐴 = ∪ 𝒫 𝐴
5		eqid 2761	. . . . 5 ⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}
6		eqid 2761	. . . . 5 ⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
7	4, 5, 6	xkoval 23635	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ↑ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
8	1, 2, 7	syl2an2 696	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
9		simpr 488	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10		fconst6g 6748	. . . . . 6 ⊢ (𝑅 ∈ Top → (𝐴 × {𝑅}):𝐴⟶Top)
11	10	adantr 484	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 × {𝑅}):𝐴⟶Top)
12		pttop 23630	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝑅}):𝐴⟶Top) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
13	9, 11, 12	syl2anc 593	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
14		elpwi 4559	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
15		restdis 23226	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
16	14, 15	sylan2 602	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
17	16	adantll 724	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
18	17	eleq1d 2846	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp))
19		discmp 23446	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Comp)
20	18, 19	bitr4di 291	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝑥 ∈ Fin))
21	20	rabbidva 3419	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin})
22		dfin5 3910	. . . . . . . . 9 ⊢ (𝒫 𝐴 ∩ Fin) = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin}
23	21, 22	eqtr4di 2814	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = (𝒫 𝐴 ∩ Fin))
24		eqidd 2762	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑅)
25		toptopon2 22966	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
26		cndis 23339	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘∪ 𝑅)) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
27	26	ancoms 462	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
28	25, 27	sylanb 590	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
29	28	rabeqdv 3428	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
30	23, 24, 29	mpoeq123dv 7466	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
31	30	rneqd 5910	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
32		eqid 2761	. . . . . . 7 ⊢ (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
33	32	rnmpo 7524	. . . . . 6 ⊢ ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}
34	31, 33	eqtrdi 2812	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}})
35		elmapi 8824	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (∪ 𝑅 ↑m 𝐴) → 𝑓:𝐴⟶∪ 𝑅)
36		eleq2 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ 𝑣 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
37	36	imbi2d 342	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
38	37	bibi1d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
39		eleq2 2850	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ ∪ 𝑅 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
40	39	imbi2d 342	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
41	40	bibi1d 345	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
42		simprl 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ (𝒫 𝐴 ∩ Fin))
43	42	elin1d 4154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ 𝒫 𝐴)
44	43	elpwid 4561	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ⊆ 𝐴)
45	44	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ 𝐴)
46	45	sselda 3934	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
47		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑘)
48	46, 47	2thd 267	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝑘))
49	48	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
50		ffvelcdm 7057	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝐴⟶∪ 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ∪ 𝑅)
51	50	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝐴⟶∪ 𝑅 → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
52	51	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
53	52	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
54		pm2.21 123	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 ∈ 𝑘 → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
55	54	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
56	53, 55	2thd 267	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
57	38, 41, 49, 56	ifbothda 4516	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
58	57	ralbidv2 3180	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
59		ffn 6686	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶∪ 𝑅 → 𝑓 Fn 𝐴)
60	59	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑓 Fn 𝐴)
61		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
62	61	elixp 8880	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
63	62	baib 543	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝐴 → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
64	60, 63	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
65		ffun 6689	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶∪ 𝑅 → Fun 𝑓)
66		fdm 6696	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴⟶∪ 𝑅 → dom 𝑓 = 𝐴)
67	66	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → dom 𝑓 = 𝐴)
68	45, 67	sseqtrrd 3971	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ dom 𝑓)
69		funimass4 6926	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝑓 ∧ 𝑘 ⊆ dom 𝑓) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
70	65, 68, 69	syl2an2 696	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
71	58, 64, 70	3bitr4d 313	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
72	35, 71	sylan2 602	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓 ∈ (∪ 𝑅 ↑m 𝐴)) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
73	72	rabbi2dva 4175	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
74		elssuni 4894	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ 𝑅 → 𝑣 ⊆ ∪ 𝑅)
75	74	ad2antll 739	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑣 ⊆ ∪ 𝑅)
76		ssid 3956	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 ⊆ ∪ 𝑅
77		sseq1 3959	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (𝑣 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
78		sseq1 3959	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (∪ 𝑅 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
79	77, 78	ifboth 4517	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ ∪ 𝑅 ∧ ∪ 𝑅 ⊆ ∪ 𝑅) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
80	75, 76, 79	sylancl 595	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
81	80	ralrimivw 3157	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
82		ss2ixp 8886	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅 → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
84		simplr 778	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝐴 ∈ 𝑉)
85		uniexg 7718	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ V)
86	85	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∪ 𝑅 ∈ V)
87		ixpconstg 8882	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑅 ∈ V) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑m 𝐴))
88	84, 86, 87	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑m 𝐴))
89	83, 88	sseqtrd 3970	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑m 𝐴))
90		sseqin2 4173	. . . . . . . . . . 11 ⊢ (X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑m 𝐴) ↔ ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
91	89, 90	sylib 220	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
92	73, 91	eqtr3d 2798	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
93	10	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝐴 × {𝑅}):𝐴⟶Top)
94	42	elin2d 4155	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ Fin)
95		simplrr 787	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → 𝑣 ∈ 𝑅)
96		eqid 2761	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑅 = ∪ 𝑅
97	96	topopn 22954	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅)
98	97	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ∪ 𝑅 ∈ 𝑅)
99	95, 98	ifcld 4524	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ 𝑅)
100		fvconst2g 7181	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
101	100	ad4ant14 762	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
102	99, 101	eleqtrrd 2864	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ ((𝐴 × {𝑅})‘𝑥))
103		eldifn 4083	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → ¬ 𝑥 ∈ 𝑘)
104	103	iffalsed 4488	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
105	104	adantl 485	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
106		eldifi 4082	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → 𝑥 ∈ 𝐴)
107	106, 101	sylan2 602	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
108	107	unieqd 4875	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ∪ ((𝐴 × {𝑅})‘𝑥) = ∪ 𝑅)
109	105, 108	eqtr4d 2799	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ ((𝐴 × {𝑅})‘𝑥))
110	84, 93, 94, 102, 109	ptopn 23631	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ (∏t‘(𝐴 × {𝑅})))
111	92, 110	eqeltrd 2861	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅})))
112		eleq1 2849	. . . . . . . 8 ⊢ (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (𝑥 ∈ (∏t‘(𝐴 × {𝑅})) ↔ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅}))))
113	111, 112	syl5ibrcom 249	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
114	113	rexlimdvva 3218	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
115	114	abssdv 4018	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ⊆ (∏t‘(𝐴 × {𝑅})))
116	34, 115	eqsstrd 3968	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅})))
117		tgfiss 23039	. . . 4 ⊢ (((∏t‘(𝐴 × {𝑅})) ∈ Top ∧ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
118	13, 116, 117	syl2anc 593	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
119	8, 118	eqsstrd 3968	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) ⊆ (∏t‘(𝐴 × {𝑅})))
120		eqid 2761	. . . . . . . 8 ⊢ (∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅}))
121	120, 96	ptuniconst 23646	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (∪ 𝑅 ↑m 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
122	121	ancoms 462	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∪ 𝑅 ↑m 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
123	28, 122	eqtrd 2796	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = ∪ (∏t‘(𝐴 × {𝑅})))
124	123	oveq2d 7407	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))))
125		eqid 2761	. . . . . 6 ⊢ ∪ (∏t‘(𝐴 × {𝑅})) = ∪ (∏t‘(𝐴 × {𝑅}))
126	125	restid 17453	. . . . 5 ⊢ ((∏t‘(𝐴 × {𝑅})) ∈ Top → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
127	13, 126	syl 17	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
128	124, 127	eqtrd 2796	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = (∏t‘(𝐴 × {𝑅})))
129	4, 120	xkoptsub 23702	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ↑ko 𝒫 𝐴))
130	1, 2, 129	syl2an2 696	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ↑ko 𝒫 𝐴))
131	128, 130	eqsstrrd 3969	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ⊆ (𝑅 ↑ko 𝒫 𝐴))
132	119, 131	eqssd 3951	1 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {cab 2739  ∀wral 3075  ∃wrex 3085  {crab 3413  Vcvv 3453   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902  ifcif 4477  𝒫 cpw 4552  {csn 4579  ∪ cuni 4862   × cxp 5641  dom cdm 5643  ran crn 5644   “ cima 5646  Fun wfun 6510   Fn wfn 6511  ⟶wf 6512  ‘cfv 6516  (class class class)co 7391   ∈ cmpo 7393   ↑_m cmap 8802  Xcixp 8873  Fincfn 8921  ficfi 9350   ↾_t crest 17440  topGenctg 17457  ∏_tcpt 17458  Topctop 22941  TopOnctopon 22958   Cn ccn 23272  Compccmp 23434   ↑_ko cxko 23609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-1st 7965  df-2nd 7966  df-1o 8431  df-2o 8432  df-map 8804  df-ixp 8874  df-en 8922  df-dom 8923  df-fin 8925  df-fi 9351  df-rest 17442  df-topgen 17463  df-pt 17464  df-top 22942  df-topon 22959  df-bases 22994  df-cn 23275  df-cmp 23435  df-xko 23611

This theorem is referenced by:  tmdgsum  24143  tmdgsum2  24144  efmndtmd  24149  symgtgp  24154