ptcnp

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

	Ref	Expression
Hypotheses	ptcnp.2	$⊢ K = \prod_{𝑡} (F)$
	ptcnp.3	$⊢ φ \to J \in TopOn (X)$
	ptcnp.4	$⊢ φ \to I \in V$
	ptcnp.5	$⊢ φ \to F : I ⟶ Top$
	ptcnp.6	$⊢ φ \to D \in X$
	ptcnp.7	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) \in (J CnP F (k)) (D)$
Assertion	ptcnp	$⊢ φ \to (x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (D)$

Proof

Step	Hyp	Ref	Expression
1		ptcnp.2	$⊢ K = \prod_{𝑡} (F)$
2		ptcnp.3	$⊢ φ \to J \in TopOn (X)$
3		ptcnp.4	$⊢ φ \to I \in V$
4		ptcnp.5	$⊢ φ \to F : I ⟶ Top$
5		ptcnp.6	$⊢ φ \to D \in X$
6		ptcnp.7	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) \in (J CnP F (k)) (D)$
7	2	adantr	$⊢ (φ \land k \in I) \to J \in TopOn (X)$
8	4	ffvelcdmda	$⊢ (φ \land k \in I) \to F (k) \in Top$
9		toptopon2	$⊢ F (k) \in Top \leftrightarrow F (k) \in TopOn (⋃ F (k))$
10	8 9	sylib	$⊢ (φ \land k \in I) \to F (k) \in TopOn (⋃ F (k))$
11		cnpf2	$⊢ (J \in TopOn (X) \land F (k) \in TopOn (⋃ F (k)) \land (x \in X ⟼ A) \in (J CnP F (k)) (D)) \to (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
12	7 10 6 11	syl3anc	$⊢ (φ \land k \in I) \to (x \in X ⟼ A) : X ⟶ ⋃ F (k)$
13	12	fvmptelcdm	$⊢ ((φ \land k \in I) \land x \in X) \to A \in ⋃ F (k)$
14	13	an32s	$⊢ ((φ \land x \in X) \land k \in I) \to A \in ⋃ F (k)$
15	14	ralrimiva	$⊢ (φ \land x \in X) \to \forall k \in I A \in ⋃ F (k)$
16	3	adantr	$⊢ (φ \land x \in X) \to I \in V$
17		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))$
18	16 17	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))$
19	15 18	mpbird	$⊢ (φ \land x \in X) \to (k \in I ⟼ A) \in \underset{k \in I}{⨉} ⋃ F (k)$
20	19	fmpttd	$⊢ φ \to (x \in X ⟼ (k \in I ⟼ A)) : X ⟶ \underset{k \in I}{⨉} ⋃ F (k)$
21		df-3an	$⊢ (g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \leftrightarrow ((g Fn I \land \forall n \in I g (n) \in F (n)) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n))$
22		nfv	$⊢ Ⅎ k (g Fn I \land \forall n \in I g (n) \in F (n))$
23		nfv	$⊢ Ⅎ k (w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n))$
24		nfcv	$⊢ \underline{Ⅎ} k X$
25		nfmpt1	$⊢ \underline{Ⅎ} k (k \in I ⟼ A)$
26	24 25	nfmpt	$⊢ \underline{Ⅎ} k (x \in X ⟼ (k \in I ⟼ A))$
27		nfcv	$⊢ \underline{Ⅎ} k D$
28	26 27	nffv	$⊢ \underline{Ⅎ} k (x \in X ⟼ (k \in I ⟼ A)) (D)$
29	28	nfel1	$⊢ Ⅎ k (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)$
30	23 29	nfan	$⊢ Ⅎ k ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n))$
31	22 30	nfan	$⊢ Ⅎ k ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))$
32		simprll	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to g Fn I$
33		simprlr	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to \forall n \in I g (n) \in F (n)$
34		fveq2	$⊢ n = k \to g (n) = g (k)$
35		fveq2	$⊢ n = k \to F (n) = F (k)$
36	34 35	eleq12d	$⊢ n = k \to (g (n) \in F (n) \leftrightarrow g (k) \in F (k))$
37	36	rspccva	$⊢ (\forall n \in I g (n) \in F (n) \land k \in I) \to g (k) \in F (k)$
38	33 37	sylan	$⊢ ((φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \land k \in I) \to g (k) \in F (k)$
39		simprrl	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to (w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n))$
40	39	simpld	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to w \in Fin$
41	39	simprd	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to \forall n \in (I ∖ w) g (n) = ⋃ F (n)$
42	35	unieqd	$⊢ n = k \to ⋃ F (n) = ⋃ F (k)$
43	34 42	eqeq12d	$⊢ n = k \to (g (n) = ⋃ F (n) \leftrightarrow g (k) = ⋃ F (k))$
44	43	rspccva	$⊢ (\forall n \in (I ∖ w) g (n) = ⋃ F (n) \land k \in (I ∖ w)) \to g (k) = ⋃ F (k)$
45	41 44	sylan	$⊢ ((φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \land k \in (I ∖ w)) \to g (k) = ⋃ F (k)$
46		simprrr	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)$
47	34	cbvixpv	$⊢ \underset{n \in I}{⨉} g (n) = \underset{k \in I}{⨉} g (k)$
48	46 47	eleqtrdi	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{k \in I}{⨉} g (k)$
49	1 2 3 4 5 6 31 32 38 40 45 48	ptcnplem	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n)))) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k))$
50	49	anassrs	$⊢ ((φ \land (g Fn I \land \forall n \in I g (n) \in F (n))) \land ((w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n))) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k))$
51	50	expr	$⊢ ((φ \land (g Fn I \land \forall n \in I g (n) \in F (n))) \land (w \in Fin \land \forall n \in (I ∖ w) g (n) = ⋃ F (n))) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k)))$
52	51	rexlimdvaa	$⊢ (φ \land (g Fn I \land \forall n \in I g (n) \in F (n))) \to (\exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k))))$
53	52	impr	$⊢ (φ \land ((g Fn I \land \forall n \in I g (n) \in F (n)) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n))) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k)))$
54	21 53	sylan2b	$⊢ (φ \land (g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n))) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k)))$
55		eleq2	$⊢ f = \underset{n \in I}{⨉} g (n) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \leftrightarrow (x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n))$
56	47	eqeq2i	$⊢ f = \underset{n \in I}{⨉} g (n) \leftrightarrow f = \underset{k \in I}{⨉} g (k)$
57	56	biimpi	$⊢ f = \underset{n \in I}{⨉} g (n) \to f = \underset{k \in I}{⨉} g (k)$
58	57	sseq2d	$⊢ f = \underset{n \in I}{⨉} g (n) \to ((x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f \leftrightarrow (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k))$
59	58	anbi2d	$⊢ f = \underset{n \in I}{⨉} g (n) \to ((D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f) \leftrightarrow (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k)))$
60	59	rexbidv	$⊢ f = \underset{n \in I}{⨉} g (n) \to (\exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f) \leftrightarrow \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k)))$
61	55 60	imbi12d	$⊢ f = \underset{n \in I}{⨉} g (n) \to (((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)) \leftrightarrow ((x \in X ⟼ (k \in I ⟼ A)) (D) \in \underset{n \in I}{⨉} g (n) \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq \underset{k \in I}{⨉} g (k))))$
62	54 61	syl5ibrcom	$⊢ (φ \land (g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n))) \to (f = \underset{n \in I}{⨉} g (n) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)))$
63	62	expimpd	$⊢ φ \to (((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land f = \underset{n \in I}{⨉} g (n)) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)))$
64	63	exlimdv	$⊢ φ \to (\exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land f = \underset{n \in I}{⨉} g (n)) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)))$
65	64	alrimiv	$⊢ φ \to \forall f (\exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land f = \underset{n \in I}{⨉} g (n)) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)))$
66		eqeq1	$⊢ a = f \to (a = \underset{n \in I}{⨉} g (n) \leftrightarrow f = \underset{n \in I}{⨉} g (n))$
67	66	anbi2d	$⊢ a = f \to (((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n)) \leftrightarrow ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land f = \underset{n \in I}{⨉} g (n)))$
68	67	exbidv	$⊢ a = f \to (\exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n)) \leftrightarrow \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land f = \underset{n \in I}{⨉} g (n)))$
69	68	ralab	$⊢ \forall f \in \{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\} ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)) \leftrightarrow \forall f (\exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land f = \underset{n \in I}{⨉} g (n)) \to ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f)))$
70	65 69	sylibr	$⊢ φ \to \forall f \in \{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\} ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f))$
71	4	ffnd	$⊢ φ \to F Fn I$
72		eqid	$⊢ \{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\} = \{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\}$
73	72	ptval	$⊢ (I \in V \land F Fn I) \to \prod_{𝑡} (F) = topGen (\{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\})$
74	3 71 73	syl2anc	$⊢ φ \to \prod_{𝑡} (F) = topGen (\{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\})$
75	1 74	eqtrid	$⊢ φ \to K = topGen (\{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\})$
76	4	feqmptd	$⊢ φ \to F = (k \in I ⟼ F (k))$
77	76	fveq2d	$⊢ φ \to \prod_{𝑡} (F) = \prod_{𝑡} ((k \in I ⟼ F (k)))$
78	1 77	eqtrid	$⊢ φ \to K = \prod_{𝑡} ((k \in I ⟼ F (k)))$
79	10	ralrimiva	$⊢ φ \to \forall k \in I F (k) \in TopOn (⋃ F (k))$
80		eqid	$⊢ \prod_{𝑡} ((k \in I ⟼ F (k))) = \prod_{𝑡} ((k \in I ⟼ F (k)))$
81	80	pttopon	$⊢ (I \in V \land \forall k \in I F (k) \in TopOn (⋃ F (k))) \to \prod_{𝑡} ((k \in I ⟼ F (k))) \in TopOn (\underset{k \in I}{⨉} ⋃ F (k))$
82	3 79 81	syl2anc	$⊢ φ \to \prod_{𝑡} ((k \in I ⟼ F (k))) \in TopOn (\underset{k \in I}{⨉} ⋃ F (k))$
83	78 82	eqeltrd	$⊢ φ \to K \in TopOn (\underset{k \in I}{⨉} ⋃ F (k))$
84	2 75 83 5	tgcnp	$⊢ φ \to ((x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (D) \leftrightarrow ((x \in X ⟼ (k \in I ⟼ A)) : X ⟶ \underset{k \in I}{⨉} ⋃ F (k) \land \forall f \in \{a \| \exists g ((g Fn I \land \forall n \in I g (n) \in F (n) \land \exists w \in Fin \forall n \in (I ∖ w) g (n) = ⋃ F (n)) \land a = \underset{n \in I}{⨉} g (n))\} ((x \in X ⟼ (k \in I ⟼ A)) (D) \in f \to \exists z \in J (D \in z \land (x \in X ⟼ (k \in I ⟼ A)) [z] \subseteq f))))$
85	20 70 84	mpbir2and	$⊢ φ \to (x \in X ⟼ (k \in I ⟼ A)) \in (J CnP K) (D)$

Metamath Proof Explorer

Theorem ptcnp

Proof