Theorem xkopt 23881

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 23220	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)
2		simpl 488	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 ∈ Top)
3		unipw 5425	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
4	3	eqcomi 2769	. . . . 5 ⊢ 𝐴 = ∪ 𝒫 𝐴
5		eqid 2760	. . . . 5 ⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}
6		eqid 2760	. . . . 5 ⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
7	4, 5, 6	xkoval 23813	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ↑ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
8	1, 2, 7	syl2an2 699	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
9		simpr 490	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10		fconst6g 6764	. . . . . 6 ⊢ (𝑅 ∈ Top → (𝐴 × {𝑅}):𝐴⟶Top)
11	10	adantr 486	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 × {𝑅}):𝐴⟶Top)
12		pttop 23808	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝑅}):𝐴⟶Top) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
13	9, 11, 12	syl2anc 596	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
14		elpwi 4564	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
15		restdis 23403	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
16	14, 15	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
17	16	adantll 727	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
18	17	eleq1d 2845	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp))
19		discmp 23623	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Comp)
20	18, 19	bitr4di 292	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝑥 ∈ Fin))
21	20	rabbidva 3418	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin})
22		dfin5 3907	. . . . . . . . 9 ⊢ (𝒫 𝐴 ∩ Fin) = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin}
23	21, 22	eqtr4di 2813	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = (𝒫 𝐴 ∩ Fin))
24		eqidd 2761	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑅)
25		toptopon2 23143	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
26		cndis 23516	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘∪ 𝑅)) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
27	26	ancoms 464	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
28	25, 27	sylanb 593	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
29	28	rabeqdv 3427	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
30	23, 24, 29	mpoeq123dv 7488	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
31	30	rneqd 5922	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
32		eqid 2760	. . . . . . 7 ⊢ (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
33	32	rnmpo 7546	. . . . . 6 ⊢ ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}
34	31, 33	eqtrdi 2811	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}})
35		elmapi 8848	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (∪ 𝑅 ↑m 𝐴) → 𝑓:𝐴⟶∪ 𝑅)
36		eleq2 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ 𝑣 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
37	36	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
38	37	bibi1d 346	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
39		eleq2 2849	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ ∪ 𝑅 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
40	39	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
41	40	bibi1d 346	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
42		simprl 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ (𝒫 𝐴 ∩ Fin))
43	42	elin1d 4150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ 𝒫 𝐴)
44	43	elpwid 4566	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ⊆ 𝐴)
45	44	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ 𝐴)
46	45	sselda 3931	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
47		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑘)
48	46, 47	2thd 268	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝑘))
49	48	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
50		ffvelcdm 7074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝐴⟶∪ 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ∪ 𝑅)
51	50	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝐴⟶∪ 𝑅 → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
52	51	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
53	52	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
54		pm2.21 124	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 ∈ 𝑘 → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
55	54	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
56	53, 55	2thd 268	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
57	38, 41, 49, 56	ifbothda 4521	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
58	57	ralbidv2 3181	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
59		ffn 6702	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶∪ 𝑅 → 𝑓 Fn 𝐴)
60	59	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑓 Fn 𝐴)
61		vex 3454	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
62	61	elixp 8911	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
63	62	baib 545	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝐴 → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
64	60, 63	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
65		ffun 6705	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶∪ 𝑅 → Fun 𝑓)
66		fdm 6712	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴⟶∪ 𝑅 → dom 𝑓 = 𝐴)
67	66	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → dom 𝑓 = 𝐴)
68	45, 67	sseqtrrd 3968	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ dom 𝑓)
69		funimass4 6942	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝑓 ∧ 𝑘 ⊆ dom 𝑓) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
70	65, 68, 69	syl2an2 699	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
71	58, 64, 70	3bitr4d 314	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
72	35, 71	sylan2 605	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓 ∈ (∪ 𝑅 ↑m 𝐴)) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
73	72	rabbi2dva 4171	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
74		elssuni 4899	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ 𝑅 → 𝑣 ⊆ ∪ 𝑅)
75	74	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑣 ⊆ ∪ 𝑅)
76		ssid 3953	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 ⊆ ∪ 𝑅
77		sseq1 3956	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (𝑣 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
78		sseq1 3956	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (∪ 𝑅 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
79	77, 78	ifboth 4522	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ ∪ 𝑅 ∧ ∪ 𝑅 ⊆ ∪ 𝑅) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
80	75, 76, 79	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
81	80	ralrimivw 3158	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
82		ss2ixp 8917	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅 → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
83	81, 82	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
84		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝐴 ∈ 𝑉)
85		uniexg 7742	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ V)
86	85	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∪ 𝑅 ∈ V)
87		ixpconstg 8913	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑅 ∈ V) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑m 𝐴))
88	84, 86, 87	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑m 𝐴))
89	83, 88	sseqtrd 3967	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑m 𝐴))
90		sseqin2 4169	. . . . . . . . . . 11 ⊢ (X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑m 𝐴) ↔ ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
91	89, 90	sylib 221	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
92	73, 91	eqtr3d 2797	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
93	10	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝐴 × {𝑅}):𝐴⟶Top)
94	42	elin2d 4151	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ Fin)
95		simplrr 790	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → 𝑣 ∈ 𝑅)
96		eqid 2760	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑅 = ∪ 𝑅
97	96	topopn 23131	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅)
98	97	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ∪ 𝑅 ∈ 𝑅)
99	95, 98	ifcld 4529	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ 𝑅)
100		fvconst2g 7201	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
101	100	ad4ant14 765	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
102	99, 101	eleqtrrd 2863	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ ((𝐴 × {𝑅})‘𝑥))
103		eldifn 4079	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → ¬ 𝑥 ∈ 𝑘)
104	103	iffalsed 4493	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
105	104	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
106		eldifi 4078	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → 𝑥 ∈ 𝐴)
107	106, 101	sylan2 605	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
108	107	unieqd 4880	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ∪ ((𝐴 × {𝑅})‘𝑥) = ∪ 𝑅)
109	105, 108	eqtr4d 2798	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ ((𝐴 × {𝑅})‘𝑥))
110	84, 93, 94, 102, 109	ptopn 23809	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ (∏t‘(𝐴 × {𝑅})))
111	92, 110	eqeltrd 2860	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅})))
112		eleq1 2848	. . . . . . . 8 ⊢ (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (𝑥 ∈ (∏t‘(𝐴 × {𝑅})) ↔ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅}))))
113	111, 112	syl5ibrcom 250	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
114	113	rexlimdvva 3219	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
115	114	abssdv 4015	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ⊆ (∏t‘(𝐴 × {𝑅})))
116	34, 115	eqsstrd 3965	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅})))
117		tgfiss 23216	. . . 4 ⊢ (((∏t‘(𝐴 × {𝑅})) ∈ Top ∧ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
118	13, 116, 117	syl2anc 596	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
119	8, 118	eqsstrd 3965	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) ⊆ (∏t‘(𝐴 × {𝑅})))
120		eqid 2760	. . . . . . . 8 ⊢ (∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅}))
121	120, 96	ptuniconst 23824	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (∪ 𝑅 ↑m 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
122	121	ancoms 464	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∪ 𝑅 ↑m 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
123	28, 122	eqtrd 2795	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = ∪ (∏t‘(𝐴 × {𝑅})))
124	123	oveq2d 7429	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))))
125		eqid 2760	. . . . . 6 ⊢ ∪ (∏t‘(𝐴 × {𝑅})) = ∪ (∏t‘(𝐴 × {𝑅}))
126	125	restid 17518	. . . . 5 ⊢ ((∏t‘(𝐴 × {𝑅})) ∈ Top → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
127	13, 126	syl 18	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
128	124, 127	eqtrd 2795	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = (∏t‘(𝐴 × {𝑅})))
129	4, 120	xkoptsub 23880	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ↑ko 𝒫 𝐴))
130	1, 2, 129	syl2an2 699	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ↑ko 𝒫 𝐴))
131	128, 130	eqsstrrd 3966	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ⊆ (𝑅 ↑ko 𝒫 𝐴))
132	119, 131	eqssd 3948	1 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ifcif 4482  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867   × cxp 5653  dom cdm 5655  ran crn 5656   “ cima 5658  Fun wfun 6527   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7413   ∈ cmpo 7415   ↑_m cmap 8826  Xcixp 8904  Fincfn 8952  ficfi 9380   ↾_t crest 17505  topGenctg 17522  ∏_tcpt 17523  Topctop 23118  TopOnctopon 23135   Cn ccn 23449  Compccmp 23611   ↑_ko cxko 23787

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 7736

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 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-1o 8455  df-2o 8456  df-map 8828  df-ixp 8905  df-en 8953  df-dom 8954  df-fin 8956  df-fi 9381  df-rest 17507  df-topgen 17528  df-pt 17529  df-top 23119  df-topon 23136  df-bases 23171  df-cn 23452  df-cmp 23612  df-xko 23789

This theorem is used by:  tmdgsum  24321  tmdgsum2  24322  efmndtmd  24327  symgtgp  24332