cnmpt2nd

Description: The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmpt21.j	$⊢ φ \to J \in TopOn (X)$
	cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
Assertion	cnmpt2nd	$⊢ φ \to (x \in X, y \in Y ⟼ y) \in ((J \times_{t} K) Cn K)$

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
3		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
4		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
5	3 4	ax-mp	$⊢ 2^{nd} Fn V$
6		ssv	$⊢ X \times Y \subseteq V$
7		fnssres	$⊢ (2^{nd} Fn V \land X \times Y \subseteq V) \to ({2^{nd} ↾}_{(X \times Y)}) Fn (X \times Y)$
8	5 6 7	mp2an	$⊢ ({2^{nd} ↾}_{(X \times Y)}) Fn (X \times Y)$
9		dffn5	$⊢ ({2^{nd} ↾}_{(X \times Y)}) Fn (X \times Y) \leftrightarrow {2^{nd} ↾}_{(X \times Y)} = (z \in (X \times Y) ⟼ ({2^{nd} ↾}_{(X \times Y)}) (z))$
10	8 9	mpbi	$⊢ {2^{nd} ↾}_{(X \times Y)} = (z \in (X \times Y) ⟼ ({2^{nd} ↾}_{(X \times Y)}) (z))$
11		fvres	$⊢ z \in (X \times Y) \to ({2^{nd} ↾}_{(X \times Y)}) (z) = 2^{nd} (z)$
12	11	mpteq2ia	$⊢ (z \in (X \times Y) ⟼ ({2^{nd} ↾}_{(X \times Y)}) (z)) = (z \in (X \times Y) ⟼ 2^{nd} (z))$
13		vex	$⊢ x \in V$
14		vex	$⊢ y \in V$
15	13 14	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
16	15	mpompt	$⊢ (z \in (X \times Y) ⟼ 2^{nd} (z)) = (x \in X, y \in Y ⟼ y)$
17	10 12 16	3eqtri	$⊢ {2^{nd} ↾}_{(X \times Y)} = (x \in X, y \in Y ⟼ y)$
18		tx2cn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to {2^{nd} ↾}_{(X \times Y)} \in ((J \times_{t} K) Cn K)$
19	1 2 18	syl2anc	$⊢ φ \to {2^{nd} ↾}_{(X \times Y)} \in ((J \times_{t} K) Cn K)$
20	17 19	eqeltrrid	$⊢ φ \to (x \in X, y \in Y ⟼ y) \in ((J \times_{t} K) Cn K)$

Metamath Proof Explorer

Theorem cnmpt2nd

Proof