tx1cn

Description: Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Assertion	tx1cn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)$

Proof

Step	Hyp	Ref	Expression
1		f1stres	$⊢ ({1^{st} ↾}_{(X \times Y)}) : X \times Y ⟶ X$
2	1	a1i	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to ({1^{st} ↾}_{(X \times Y)}) : X \times Y ⟶ X$
3		ffn	$⊢ ({1^{st} ↾}_{(X \times Y)}) : X \times Y ⟶ X \to ({1^{st} ↾}_{(X \times Y)}) Fn (X \times Y)$
4		elpreima	$⊢ ({1^{st} ↾}_{(X \times Y)}) Fn (X \times Y) \to (z \in {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \leftrightarrow (z \in (X \times Y) \land ({1^{st} ↾}_{(X \times Y)}) (z) \in w))$
5	1 3 4	mp2b	$⊢ z \in {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \leftrightarrow (z \in (X \times Y) \land ({1^{st} ↾}_{(X \times Y)}) (z) \in w)$
6		fvres	$⊢ z \in (X \times Y) \to ({1^{st} ↾}_{(X \times Y)}) (z) = 1^{st} (z)$
7	6	eleq1d	$⊢ z \in (X \times Y) \to (({1^{st} ↾}_{(X \times Y)}) (z) \in w \leftrightarrow 1^{st} (z) \in w)$
8		1st2nd2	$⊢ z \in (X \times Y) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
9		xp2nd	$⊢ z \in (X \times Y) \to 2^{nd} (z) \in Y$
10		elxp6	$⊢ z \in (w \times Y) \leftrightarrow (z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land (1^{st} (z) \in w \land 2^{nd} (z) \in Y))$
11		anass	$⊢ ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 1^{st} (z) \in w) \land 2^{nd} (z) \in Y) \leftrightarrow (z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land (1^{st} (z) \in w \land 2^{nd} (z) \in Y))$
12		an32	$⊢ ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 1^{st} (z) \in w) \land 2^{nd} (z) \in Y) \leftrightarrow ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 2^{nd} (z) \in Y) \land 1^{st} (z) \in w)$
13	10 11 12	3bitr2i	$⊢ z \in (w \times Y) \leftrightarrow ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 2^{nd} (z) \in Y) \land 1^{st} (z) \in w)$
14	13	baib	$⊢ (z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 2^{nd} (z) \in Y) \to (z \in (w \times Y) \leftrightarrow 1^{st} (z) \in w)$
15	8 9 14	syl2anc	$⊢ z \in (X \times Y) \to (z \in (w \times Y) \leftrightarrow 1^{st} (z) \in w)$
16	7 15	bitr4d	$⊢ z \in (X \times Y) \to (({1^{st} ↾}_{(X \times Y)}) (z) \in w \leftrightarrow z \in (w \times Y))$
17	16	pm5.32i	$⊢ (z \in (X \times Y) \land ({1^{st} ↾}_{(X \times Y)}) (z) \in w) \leftrightarrow (z \in (X \times Y) \land z \in (w \times Y))$
18	5 17	bitri	$⊢ z \in {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \leftrightarrow (z \in (X \times Y) \land z \in (w \times Y))$
19		toponss	$⊢ (R \in TopOn (X) \land w \in R) \to w \subseteq X$
20	19	adantlr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to w \subseteq X$
21		xpss1	$⊢ w \subseteq X \to w \times Y \subseteq X \times Y$
22	20 21	syl	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to w \times Y \subseteq X \times Y$
23	22	sseld	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to (z \in (w \times Y) \to z \in (X \times Y))$
24	23	pm4.71rd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to (z \in (w \times Y) \leftrightarrow (z \in (X \times Y) \land z \in (w \times Y)))$
25	18 24	bitr4id	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to (z \in {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \leftrightarrow z \in (w \times Y))$
26	25	eqrdv	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] = w \times Y$
27		toponmax	$⊢ S \in TopOn (Y) \to Y \in S$
28	27	ad2antlr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to Y \in S$
29		txopn	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (w \in R \land Y \in S)) \to w \times Y \in (R \times_{t} S)$
30	29	anassrs	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \land Y \in S) \to w \times Y \in (R \times_{t} S)$
31	28 30	mpdan	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to w \times Y \in (R \times_{t} S)$
32	26 31	eqeltrd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land w \in R) \to {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \in (R \times_{t} S)$
33	32	ralrimiva	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to \forall w \in R {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \in (R \times_{t} S)$
34		txtopon	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to R \times_{t} S \in TopOn (X \times Y)$
35		simpl	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to R \in TopOn (X)$
36		iscn	$⊢ (R \times_{t} S \in TopOn (X \times Y) \land R \in TopOn (X)) \to ({1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R) \leftrightarrow (({1^{st} ↾}_{(X \times Y)}) : X \times Y ⟶ X \land \forall w \in R {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \in (R \times_{t} S)))$
37	34 35 36	syl2anc	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to ({1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R) \leftrightarrow (({1^{st} ↾}_{(X \times Y)}) : X \times Y ⟶ X \land \forall w \in R {({1^{st} ↾}_{(X \times Y)})}^{-1} [w] \in (R \times_{t} S)))$
38	2 33 37	mpbir2and	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)$

Metamath Proof Explorer

Theorem tx1cn

Proof