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	$⊢ K = \prod_{𝑡} (F)$
	ptcn.3	$⊢ φ \to J \in TopOn (X)$
	ptcn.4	$⊢ φ \to I \in V$
	ptcn.5	$⊢ φ \to F : I ⟶ Top$
	ptcn.6	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) \in (J Cn F (k))$
Assertion	ptcn	$⊢ φ \to (x \in X ⟼ (k \in I ⟼ A)) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ptcn.2	$⊢ K = \prod_{𝑡} (F)$
2		ptcn.3	$⊢ φ \to J \in TopOn (X)$
3		ptcn.4	$⊢ φ \to I \in V$
4		ptcn.5	$⊢ φ \to F : I ⟶ Top$
5		ptcn.6	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) \in (J Cn F (k))$
6	2	adantr	$⊢ (φ \land k \in I) \to J \in TopOn (X)$
7	4	ffvelcdmda	$⊢ (φ \land k \in I) \to F (k) \in Top$
8		toptopon2	$⊢ F (k) \in Top \leftrightarrow F (k) \in TopOn (⋃ F (k))$
9	7 8	sylib	$⊢ (φ \land k \in I) \to F (k) \in TopOn (⋃ F (k))$
10		cnf2	$⊢ (J \in TopOn (X) \land F (k) \in TopOn (⋃ F (k)) \land (x \in X ⟼ A) \in (J Cn F (k))) \to (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
11	6 9 5 10	syl3anc	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
12	11	fvmptelcdm	$⊢ ((φ \land k \in I) \land x \in X) \to A \in ⋃ F (k)$
13	12	an32s	$⊢ ((φ \land x \in X) \land k \in I) \to A \in ⋃ F (k)$
14	13	ralrimiva	$⊢ (φ \land x \in X) \to \forall k \in I A \in ⋃ F (k)$
15	3	adantr	$⊢ (φ \land x \in X) \to I \in V$
16		mptelixpg	$⊢ I \in V \to ((k \in I ⟼ A) \in \underset{k \in I}{⨉} ⋃ F (k) \leftrightarrow \forall k \in I A \in ⋃ F (k))$
17	15 16	syl	$⊢ (φ \land x \in X) \to ((k \in I ⟼ A) \in \underset{k \in I}{⨉} ⋃ F (k) \leftrightarrow \forall k \in I A \in ⋃ F (k))$
18	14 17	mpbird	$⊢ (φ \land x \in X) \to (k \in I ⟼ A) \in \underset{k \in I}{⨉} ⋃ F (k)$
19	1	ptuni	$⊢ (I \in V \land F : I ⟶ Top) \to \underset{k \in I}{⨉} ⋃ F (k) = ⋃ K$
20	3 4 19	syl2anc	$⊢ φ \to \underset{k \in I}{⨉} ⋃ F (k) = ⋃ K$
21	20	adantr	$⊢ (φ \land x \in X) \to \underset{k \in I}{⨉} ⋃ F (k) = ⋃ K$
22	18 21	eleqtrd	$⊢ (φ \land x \in X) \to (k \in I ⟼ A) \in ⋃ K$
23	22	fmpttd	$⊢ φ \to (x \in X ⟼ (k \in I ⟼ A)) : X ⟶ ⋃ K$
24	2	adantr	$⊢ (φ \land z \in X) \to J \in TopOn (X)$
25	3	adantr	$⊢ (φ \land z \in X) \to I \in V$
26	4	adantr	$⊢ (φ \land z \in X) \to F : I ⟶ Top$
27		simpr	$⊢ (φ \land z \in X) \to z \in X$
28	5	adantlr	$⊢ ((φ \land z \in X) \land k \in I) \to (x \in X ⟼ A) \in (J Cn F (k))$
29		simplr	$⊢ ((φ \land z \in X) \land k \in I) \to z \in X$
30		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
31	2 30	syl	$⊢ φ \to X = ⋃ J$
32	31	ad2antrr	$⊢ ((φ \land z \in X) \land k \in I) \to X = ⋃ J$
33	29 32	eleqtrd	$⊢ ((φ \land z \in X) \land k \in I) \to z \in ⋃ J$
34		eqid	$⊢ ⋃ J = ⋃ J$
35	34	cncnpi	$⊢ ((x \in X ⟼ A) \in (J Cn F (k)) \land z \in ⋃ J) \to (x \in X ⟼ A) \in (J CnP F (k)) (z)$
36	28 33 35	syl2anc	$⊢ ((φ \land z \in X) \land k \in I) \to (x \in X ⟼ A) \in (J CnP F (k)) (z)$
37	1 24 25 26 27 36	ptcnp	$⊢ (φ \land z \in X) \to (x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (z)$
38	37	ralrimiva	$⊢ φ \to \forall z \in X (x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (z)$
39		pttop	$⊢ (I \in V \land F : I ⟶ Top) \to \prod_{𝑡} (F) \in Top$
40	3 4 39	syl2anc	$⊢ φ \to \prod_{𝑡} (F) \in Top$
41	1 40	eqeltrid	$⊢ φ \to K \in Top$
42		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
43	41 42	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
44		cncnp	$⊢ (J \in TopOn (X) \land K \in TopOn (⋃ K)) \to ((x \in X ⟼ (k \in I ⟼ A)) \in (J Cn K) \leftrightarrow ((x \in X ⟼ (k \in I ⟼ A)) : X ⟶ ⋃ K \land \forall z \in X (x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (z)))$
45	2 43 44	syl2anc	$⊢ φ \to ((x \in X ⟼ (k \in I ⟼ A)) \in (J Cn K) \leftrightarrow ((x \in X ⟼ (k \in I ⟼ A)) : X ⟶ ⋃ K \land \forall z \in X (x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (z)))$
46	23 38 45	mpbir2and	$⊢ φ \to (x \in X ⟼ (k \in I ⟼ A)) \in (J Cn K)$

Metamath Proof Explorer

Theorem ptcn

Proof