# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpt21.k ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
Assertion cnmpt1st ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{x}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{J}\right)$

### Proof

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