Theorem xkopt 22806

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 22145	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)
2		simpl 483	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 ∈ Top)
3		unipw 5366	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
4	3	eqcomi 2747	. . . . 5 ⊢ 𝐴 = ∪ 𝒫 𝐴
5		eqid 2738	. . . . 5 ⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}
6		eqid 2738	. . . . 5 ⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
7	4, 5, 6	xkoval 22738	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ↑ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
8	1, 2, 7	syl2an2 683	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
9		simpr 485	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10		fconst6g 6663	. . . . . 6 ⊢ (𝑅 ∈ Top → (𝐴 × {𝑅}):𝐴⟶Top)
11	10	adantr 481	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 × {𝑅}):𝐴⟶Top)
12		pttop 22733	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝑅}):𝐴⟶Top) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
13	9, 11, 12	syl2anc 584	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
14		elpwi 4542	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
15		restdis 22329	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
16	14, 15	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
17	16	adantll 711	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥)
18	17	eleq1d 2823	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp))
19		discmp 22549	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Comp)
20	18, 19	bitr4di 289	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝑥 ∈ Fin))
21	20	rabbidva 3413	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin})
22		dfin5 3895	. . . . . . . . 9 ⊢ (𝒫 𝐴 ∩ Fin) = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin}
23	21, 22	eqtr4di 2796	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = (𝒫 𝐴 ∩ Fin))
24		eqidd 2739	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑅)
25		toptopon2 22067	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
26		cndis 22442	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘∪ 𝑅)) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
27	26	ancoms 459	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
28	25, 27	sylanb 581	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑m 𝐴))
29	28	rabeqdv 3419	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
30	23, 24, 29	mpoeq123dv 7350	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
31	30	rneqd 5847	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
32		eqid 2738	. . . . . . 7 ⊢ (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
33	32	rnmpo 7407	. . . . . 6 ⊢ ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}
34	31, 33	eqtrdi 2794	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}})
35		elmapi 8637	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (∪ 𝑅 ↑m 𝐴) → 𝑓:𝐴⟶∪ 𝑅)
36		eleq2 2827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ 𝑣 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
37	36	imbi2d 341	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
38	37	bibi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
39		eleq2 2827	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ ∪ 𝑅 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
40	39	imbi2d 341	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))))
41	40	bibi1d 344	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))))
42		simprl 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ (𝒫 𝐴 ∩ Fin))
43	42	elin1d 4132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ 𝒫 𝐴)
44	43	elpwid 4544	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ⊆ 𝐴)
45	44	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ 𝐴)
46	45	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
47		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑘)
48	46, 47	2thd 264	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝑘))
49	48	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
50		ffvelrn 6959	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝐴⟶∪ 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ∪ 𝑅)
51	50	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝐴⟶∪ 𝑅 → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
52	51	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
53	52	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅))
54		pm2.21 123	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 ∈ 𝑘 → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
55	54	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))
56	53, 55	2thd 264	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
57	38, 41, 49, 56	ifbothda 4497	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))
58	57	ralbidv2 3110	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
59		ffn 6600	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶∪ 𝑅 → 𝑓 Fn 𝐴)
60	59	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑓 Fn 𝐴)
61		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
62	61	elixp 8692	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
63	62	baib 536	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝐴 → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
64	60, 63	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))
65		ffun 6603	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶∪ 𝑅 → Fun 𝑓)
66		fdm 6609	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴⟶∪ 𝑅 → dom 𝑓 = 𝐴)
67	66	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → dom 𝑓 = 𝐴)
68	45, 67	sseqtrrd 3962	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ dom 𝑓)
69		funimass4 6834	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝑓 ∧ 𝑘 ⊆ dom 𝑓) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
70	65, 68, 69	syl2an2 683	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣))
71	58, 64, 70	3bitr4d 311	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
72	35, 71	sylan2 593	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓 ∈ (∪ 𝑅 ↑m 𝐴)) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣))
73	72	rabbi2dva 4151	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
74		elssuni 4871	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ 𝑅 → 𝑣 ⊆ ∪ 𝑅)
75	74	ad2antll 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑣 ⊆ ∪ 𝑅)
76		ssid 3943	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 ⊆ ∪ 𝑅
77		sseq1 3946	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (𝑣 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
78		sseq1 3946	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑅 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (∪ 𝑅 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅))
79	77, 78	ifboth 4498	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ ∪ 𝑅 ∧ ∪ 𝑅 ⊆ ∪ 𝑅) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
80	75, 76, 79	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
81	80	ralrimivw 3104	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)
82		ss2ixp 8698	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅 → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈ 𝐴 ∪ 𝑅)
84		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝐴 ∈ 𝑉)
85		uniexg 7593	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ V)
86	85	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∪ 𝑅 ∈ V)
87		ixpconstg 8694	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑅 ∈ V) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑m 𝐴))
88	84, 86, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪ 𝑅 ↑m 𝐴))
89	83, 88	sseqtrd 3961	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑m 𝐴))
90		sseqin2 4149	. . . . . . . . . . 11 ⊢ (X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅 ↑m 𝐴) ↔ ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
91	89, 90	sylib 217	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪ 𝑅 ↑m 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
92	73, 91	eqtr3d 2780	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))
93	10	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝐴 × {𝑅}):𝐴⟶Top)
94	42	elin2d 4133	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ Fin)
95		simplrr 775	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → 𝑣 ∈ 𝑅)
96		eqid 2738	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑅 = ∪ 𝑅
97	96	topopn 22055	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅)
98	97	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ∪ 𝑅 ∈ 𝑅)
99	95, 98	ifcld 4505	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ 𝑅)
100		fvconst2g 7077	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Top ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
101	100	ad4ant14 749	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
102	99, 101	eleqtrrd 2842	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ ((𝐴 × {𝑅})‘𝑥))
103		eldifn 4062	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → ¬ 𝑥 ∈ 𝑘)
104	103	iffalsed 4470	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
105	104	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ 𝑅)
106		eldifi 4061	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → 𝑥 ∈ 𝐴)
107	106, 101	sylan2 593	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
108	107	unieqd 4853	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ∪ ((𝐴 × {𝑅})‘𝑥) = ∪ 𝑅)
109	105, 108	eqtr4d 2781	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪ ((𝐴 × {𝑅})‘𝑥))
110	84, 93, 94, 102, 109	ptopn 22734	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ (∏t‘(𝐴 × {𝑅})))
111	92, 110	eqeltrd 2839	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅})))
112		eleq1 2826	. . . . . . . 8 ⊢ (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (𝑥 ∈ (∏t‘(𝐴 × {𝑅})) ↔ {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅}))))
113	111, 112	syl5ibrcom 246	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
114	113	rexlimdvva 3223	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
115	114	abssdv 4002	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑m 𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ⊆ (∏t‘(𝐴 × {𝑅})))
116	34, 115	eqsstrd 3959	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅})))
117		tgfiss 22141	. . . 4 ⊢ (((∏t‘(𝐴 × {𝑅})) ∈ Top ∧ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
118	13, 116, 117	syl2anc 584	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
119	8, 118	eqsstrd 3959	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) ⊆ (∏t‘(𝐴 × {𝑅})))
120		eqid 2738	. . . . . . . 8 ⊢ (∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅}))
121	120, 96	ptuniconst 22749	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (∪ 𝑅 ↑m 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
122	121	ancoms 459	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∪ 𝑅 ↑m 𝐴) = ∪ (∏t‘(𝐴 × {𝑅})))
123	28, 122	eqtrd 2778	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = ∪ (∏t‘(𝐴 × {𝑅})))
124	123	oveq2d 7291	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))))
125		eqid 2738	. . . . . 6 ⊢ ∪ (∏t‘(𝐴 × {𝑅})) = ∪ (∏t‘(𝐴 × {𝑅}))
126	125	restid 17144	. . . . 5 ⊢ ((∏t‘(𝐴 × {𝑅})) ∈ Top → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
127	13, 126	syl 17	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
128	124, 127	eqtrd 2778	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = (∏t‘(𝐴 × {𝑅})))
129	4, 120	xkoptsub 22805	. . . 4 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ↑ko 𝒫 𝐴))
130	1, 2, 129	syl2an2 683	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ↑ko 𝒫 𝐴))
131	128, 130	eqsstrrd 3960	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ⊆ (𝑅 ↑ko 𝒫 𝐴))
132	119, 131	eqssd 3938	1 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {cab 2715  ∀wral 3064  ∃wrex 3065  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∩ cin 3886   ⊆ wss 3887  ifcif 4459  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839   × cxp 5587  dom cdm 5589  ran crn 5590   “ cima 5592  Fun wfun 6427   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277   ↑_m cmap 8615  Xcixp 8685  Fincfn 8733  ficfi 9169   ↾_t crest 17131  topGenctg 17148  ∏_tcpt 17149  Topctop 22042  TopOnctopon 22059   Cn ccn 22375  Compccmp 22537   ↑_ko cxko 22712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-1o 8297  df-er 8498  df-map 8617  df-ixp 8686  df-en 8734  df-dom 8735  df-fin 8737  df-fi 9170  df-rest 17133  df-topgen 17154  df-pt 17155  df-top 22043  df-topon 22060  df-bases 22096  df-cn 22378  df-cmp 22538  df-xko 22714

This theorem is referenced by:  tmdgsum  23246  tmdgsum2  23247  efmndtmd  23252  symgtgp  23257