cnmpt1st

Description: The projection onto the first 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	cnmpt1st	$⊢ φ \to (x \in X, y \in Y ⟼ x) \in ((J \times_{t} K) Cn J)$

Proof

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

Metamath Proof Explorer

Theorem cnmpt1st

Proof