ptcn

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

	Ref	Expression
Hypotheses	ptcn.2	⊢ 𝐾 = ( ∏_t ‘ 𝐹 )
	ptcn.3	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	ptcn.4	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	ptcn.5	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
	ptcn.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) )
Assertion	ptcn	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		ptcn.2	⊢ 𝐾 = ( ∏_t ‘ 𝐹 )
2		ptcn.3	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		ptcn.4	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		ptcn.5	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
5		ptcn.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
8		toptopon2	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
9	7 8	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
10		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
11	6 9 5 10	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
12	11	fvmptelcdm	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
13	12	an32s	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
14	13	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
15	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
16		mptelixpg	⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
18	14 17	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) )
19	1	ptuni	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ Top ) → X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
20	3 4 19	syl2anc	⊢ ( 𝜑 → X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
22	18 21	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ ∪ 𝐾 )
23	22	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐾 )
24	2	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
25	3	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
26	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐹 : 𝐼 ⟶ Top )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
28	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) )
29		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑧 ∈ 𝑋 )
30		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
31	2 30	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
32	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑋 = ∪ 𝐽 )
33	29 32	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑧 ∈ ∪ 𝐽 )
34		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
35	34	cncnpi	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑧 ∈ ∪ 𝐽 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) )
36	28 33 35	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) )
37	1 24 25 26 27 36	ptcnp	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) )
38	37	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) )
39		pttop	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ Top ) → ( ∏_t ‘ 𝐹 ) ∈ Top )
40	3 4 39	syl2anc	⊢ ( 𝜑 → ( ∏_t ‘ 𝐹 ) ∈ Top )
41	1 40	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ Top )
42		toptopon2	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
43	41 42	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
44		cncnp	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐾 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) ) ) )
45	2 43 44	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐾 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) ) ) )
46	23 38 45	mpbir2and	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )

Metamath Proof Explorer

Theorem ptcn

Proof