Theorem ptcnp 21235

Description: If every projection of a function is continuous at 𝐷, then the function itself is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)

Hypotheses

Ref	Expression
ptcnp.2	⊢ 𝐾 = (∏t‘𝐹)
ptcnp.3	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
ptcnp.4	⊢ (𝜑 → 𝐼 ∈ 𝑉)
ptcnp.5	⊢ (𝜑 → 𝐹:𝐼⟶Top)
ptcnp.6	⊢ (𝜑 → 𝐷 ∈ 𝑋)
ptcnp.7	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))

Assertion

Ref	Expression
ptcnp	⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷))

Distinct variable groups:   𝑥,𝑘,𝐷   𝑘,𝐼,𝑥   𝑘,𝐽   𝜑,𝑘,𝑥   𝑘,𝐹,𝑥   𝑘,𝑉,𝑥   𝑘,𝑋,𝑥

Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐽(𝑥)   𝐾(𝑥,𝑘)

Proof of Theorem ptcnp

Dummy variables 𝑓 𝑔 𝑤 𝑧 𝑎 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcnp.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
2	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋))
3		ptcnp.5	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐼⟶Top)
4	3	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top)
5		eqid 2610	. . . . . . . . . . 11 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
6	5	toptopon 20548	. . . . . . . . . 10 ⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
7	4, 6	sylib 207	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
8		ptcnp.7	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
9		cnpf2 20864	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
10	2, 7, 8, 9	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
11		eqid 2610	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴)
12	11	fmpt 6289	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘) ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
13	10, 12	sylibr 223	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ (𝐹‘𝑘))
14	13	r19.21bi 2916	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘))
15	14	an32s 842	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → 𝐴 ∈ ∪ (𝐹‘𝑘))
16	15	ralrimiva 2949	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑘 ∈ 𝐼 𝐴 ∈ ∪ (𝐹‘𝑘))
17		ptcnp.4	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
18	17	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉)
19		mptelixpg 7831	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ ∪ (𝐹‘𝑘)))
20	18, 19	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ ∪ (𝐹‘𝑘)))
21	16, 20	mpbird 246	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘))
22		eqid 2610	. . 3 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
23	21, 22	fmptd 6292	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)):𝑋⟶X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘))
24		df-3an 1033	. . . . . . . 8 ⊢ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)))
25		ptcnp.2	. . . . . . . . . . . . 13 ⊢ 𝐾 = (∏t‘𝐹)
26		ptcnp.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
27		nfv 1830	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))
28		nfv 1830	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))
29		nfcv 2751	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘𝑋
30		nfmpt1 4675	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝑘 ∈ 𝐼 ↦ 𝐴)
31	29, 30	nfmpt 4674	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
32		nfcv 2751	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘𝐷
33	31, 32	nffv 6110	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
34	33	nfel1 2765	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)
35	28, 34	nfan 1816	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛))
36	27, 35	nfan 1816	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))
37		simprll 798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → 𝑔 Fn 𝐼)
38		simprlr 799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))
39		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝑔‘𝑛) = (𝑔‘𝑘))
40		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
41	39, 40	eleq12d 2682	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝑔‘𝑘) ∈ (𝐹‘𝑘)))
42	41	rspccva 3281	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) ∈ (𝐹‘𝑘))
43	38, 42	sylan 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) ∈ (𝐹‘𝑘))
44		simprrl 800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → (𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)))
45	44	simpld 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → 𝑤 ∈ Fin)
46	44	simprd 478	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))
47	40	unieqd 4382	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
48	39, 47	eqeq12d 2625	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑔‘𝑛) = ∪ (𝐹‘𝑛) ↔ (𝑔‘𝑘) = ∪ (𝐹‘𝑘)))
49	48	rspccva 3281	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛) ∧ 𝑘 ∈ (𝐼 ∖ 𝑤)) → (𝑔‘𝑘) = ∪ (𝐹‘𝑘))
50	46, 49	sylan 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) ∧ 𝑘 ∈ (𝐼 ∖ 𝑤)) → (𝑔‘𝑘) = ∪ (𝐹‘𝑘))
51		simprrr 801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛))
52	39	cbvixpv 7812	. . . . . . . . . . . . . 14 ⊢ X𝑛 ∈ 𝐼 (𝑔‘𝑛) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)
53	51, 52	syl6eleq 2698	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝑔‘𝑘))
54	25, 1, 17, 3, 26, 8, 36, 37, 43, 45, 50, 53	ptcnplem 21234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
55	54	anassrs 678	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
56	55	expr 641	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ∧ (𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
57	56	rexlimdvaa 3014	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))) → (∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
58	57	impr 647	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
59	24, 58	sylan2b 491	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
60		eleq2 2677	. . . . . . . 8 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))
61	52	eqeq2i 2622	. . . . . . . . . . . 12 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) ↔ 𝑓 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))
62	61	biimpi 205	. . . . . . . . . . 11 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → 𝑓 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))
63	62	sseq2d 3596	. . . . . . . . . 10 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓 ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
64	63	anbi2d 736	. . . . . . . . 9 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓) ↔ (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
65	64	rexbidv 3034	. . . . . . . 8 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓) ↔ ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
66	60, 65	imbi12d 333	. . . . . . 7 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ((((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)) ↔ (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
67	59, 66	syl5ibrcom 236	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
68	67	expimpd 627	. . . . 5 ⊢ (𝜑 → (((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
69	68	exlimdv 1848	. . . 4 ⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
70	69	alrimiv 1842	. . 3 ⊢ (𝜑 → ∀𝑓(∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
71		eqeq1 2614	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) ↔ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)))
72	71	anbi2d 736	. . . . 5 ⊢ (𝑎 = 𝑓 → (((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))))
73	72	exbidv 1837	. . . 4 ⊢ (𝑎 = 𝑓 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))))
74	73	ralab 3334	. . 3 ⊢ (∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)) ↔ ∀𝑓(∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
75	70, 74	sylibr 223	. 2 ⊢ (𝜑 → ∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)))
76		ffn 5958	. . . . . 6 ⊢ (𝐹:𝐼⟶Top → 𝐹 Fn 𝐼)
77	3, 76	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐼)
78		eqid 2610	. . . . . 6 ⊢ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} = {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}
79	78	ptval 21183	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 Fn 𝐼) → (∏t‘𝐹) = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}))
80	17, 77, 79	syl2anc 691	. . . 4 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}))
81	25, 80	syl5eq 2656	. . 3 ⊢ (𝜑 → 𝐾 = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}))
82	3	feqmptd 6159	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘)))
83	82	fveq2d 6107	. . . . 5 ⊢ (𝜑 → (∏t‘𝐹) = (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))))
84	25, 83	syl5eq 2656	. . . 4 ⊢ (𝜑 → 𝐾 = (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))))
85	7	ralrimiva 2949	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
86		eqid 2610	. . . . . 6 ⊢ (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) = (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘)))
87	86	pttopon 21209	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘))) → (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) ∈ (TopOn‘X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘)))
88	17, 85, 87	syl2anc 691	. . . 4 ⊢ (𝜑 → (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) ∈ (TopOn‘X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘)))
89	84, 88	eqeltrd 2688	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘)))
90	1, 81, 89, 26	tgcnp 20867	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)):𝑋⟶X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘) ∧ ∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)))))
91	23, 75, 90	mpbir2and 959	1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ⊆ wss 3540  ∪ cuni 4372   ↦ cmpt 4643   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Xcixp 7794  Fincfn 7841  topGenctg 15921  ∏_tcpt 15922  Topctop 20517  TopOnctopon 20518   CnP ccnp 20839

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-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-fin 7845  df-fi 8200  df-topgen 15927  df-pt 15928  df-top 20521  df-bases 20522  df-topon 20523  df-cnp 20842

This theorem is referenced by:  ptcn  21240