tx2cn

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

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

Proof

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

Metamath Proof Explorer

Theorem tx2cn

Proof