ptpjcn

Description: Continuity of a projection map into a topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Hypotheses	ptpjcn.1	$⊢ Y = ⋃ J$
	ptpjcn.2	$⊢ J = \prod_{𝑡} (F)$
Assertion	ptpjcn	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (x \in Y ⟼ x (I)) \in (J Cn F (I))$

Proof

Step	Hyp	Ref	Expression
1		ptpjcn.1	$⊢ Y = ⋃ J$
2		ptpjcn.2	$⊢ J = \prod_{𝑡} (F)$
3	2	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ J$
4	3	3adant3	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ J$
5	1 4	eqtr4id	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to Y = \underset{k \in A}{⨉} ⋃ F (k)$
6	5	mpteq1d	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (x \in Y ⟼ x (I)) = (x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))$
7		pttop	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) \in Top$
8	7	3adant3	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to \prod_{𝑡} (F) \in Top$
9	2 8	eqeltrid	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to J \in Top$
10		ffvelcdm	$⊢ (F : A ⟶ Top \land I \in A) \to F (I) \in Top$
11	10	3adant1	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to F (I) \in Top$
12		vex	$⊢ x \in V$
13	12	elixp	$⊢ x \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow (x Fn A \land \forall k \in A x (k) \in ⋃ F (k))$
14	13	simprbi	$⊢ x \in \underset{k \in A}{⨉} ⋃ F (k) \to \forall k \in A x (k) \in ⋃ F (k)$
15		fveq2	$⊢ k = I \to x (k) = x (I)$
16		fveq2	$⊢ k = I \to F (k) = F (I)$
17	16	unieqd	$⊢ k = I \to ⋃ F (k) = ⋃ F (I)$
18	15 17	eleq12d	$⊢ k = I \to (x (k) \in ⋃ F (k) \leftrightarrow x (I) \in ⋃ F (I))$
19	18	rspcva	$⊢ (I \in A \land \forall k \in A x (k) \in ⋃ F (k)) \to x (I) \in ⋃ F (I)$
20	14 19	sylan2	$⊢ (I \in A \land x \in \underset{k \in A}{⨉} ⋃ F (k)) \to x (I) \in ⋃ F (I)$
21	20	3ad2antl3	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land x \in \underset{k \in A}{⨉} ⋃ F (k)) \to x (I) \in ⋃ F (I)$
22	21	fmpttd	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) : \underset{k \in A}{⨉} ⋃ F (k) ⟶ ⋃ F (I)$
23	5	feq2d	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to ((x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) : Y ⟶ ⋃ F (I) \leftrightarrow (x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) : \underset{k \in A}{⨉} ⋃ F (k) ⟶ ⋃ F (I))$
24	22 23	mpbird	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) : Y ⟶ ⋃ F (I)$
25		eqid	$⊢ \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} = \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\}$
26	25	ptbas	$⊢ (A \in V \land F : A ⟶ Top) \to \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} \in TopBases$
27		bastg	$⊢ \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} \in TopBases \to \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} \subseteq topGen (\{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\})$
28	26 27	syl	$⊢ (A \in V \land F : A ⟶ Top) \to \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} \subseteq topGen (\{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\})$
29		ffn	$⊢ F : A ⟶ Top \to F Fn A$
30	25	ptval	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (\{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\})$
31	2 30	eqtrid	$⊢ (A \in V \land F Fn A) \to J = topGen (\{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\})$
32	29 31	sylan2	$⊢ (A \in V \land F : A ⟶ Top) \to J = topGen (\{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\})$
33	28 32	sseqtrrd	$⊢ (A \in V \land F : A ⟶ Top) \to \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} \subseteq J$
34	33	adantr	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land u \in F (I))) \to \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\} \subseteq J$
35		eqid	$⊢ \underset{k \in A}{⨉} ⋃ F (k) = \underset{k \in A}{⨉} ⋃ F (k)$
36	25 35	ptpjpre2	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land u \in F (I))) \to {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in \{w \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))\}$
37	34 36	sseldd	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land u \in F (I))) \to {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in J$
38	37	expr	$⊢ ((A \in V \land F : A ⟶ Top) \land I \in A) \to (u \in F (I) \to {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in J)$
39	38	ralrimiv	$⊢ ((A \in V \land F : A ⟶ Top) \land I \in A) \to \forall u \in F (I) {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in J$
40	39	3impa	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to \forall u \in F (I) {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in J$
41	24 40	jca	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to ((x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) : Y ⟶ ⋃ F (I) \land \forall u \in F (I) {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in J)$
42		eqid	$⊢ ⋃ F (I) = ⋃ F (I)$
43	1 42	iscn2	$⊢ (x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) \in (J Cn F (I)) \leftrightarrow ((J \in Top \land F (I) \in Top) \land ((x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) : Y ⟶ ⋃ F (I) \land \forall u \in F (I) {(x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I))}^{-1} [u] \in J))$
44	9 11 41 43	syl21anbrc	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (x \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ x (I)) \in (J Cn F (I))$
45	6 44	eqeltrd	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (x \in Y ⟼ x (I)) \in (J Cn F (I))$

Metamath Proof Explorer

Theorem ptpjcn

Proof