# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpt21.k ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
Assertion cnmpt2nd ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{y}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{K}\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 fo2nd ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$
4 fofn ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {2}^{nd}Fn\mathrm{V}$
5 3 4 ax-mp ${⊢}{2}^{nd}Fn\mathrm{V}$
6 ssv ${⊢}{X}×{Y}\subseteq \mathrm{V}$
7 fnssres ${⊢}\left({2}^{nd}Fn\mathrm{V}\wedge {X}×{Y}\subseteq \mathrm{V}\right)\to \left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)Fn\left({X}×{Y}\right)$
8 5 6 7 mp2an ${⊢}\left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)Fn\left({X}×{Y}\right)$
9 dffn5 ${⊢}\left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)Fn\left({X}×{Y}\right)↔{{2}^{nd}↾}_{\left({X}×{Y}\right)}=\left({z}\in \left({X}×{Y}\right)⟼\left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)\left({z}\right)\right)$
10 8 9 mpbi ${⊢}{{2}^{nd}↾}_{\left({X}×{Y}\right)}=\left({z}\in \left({X}×{Y}\right)⟼\left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)\left({z}\right)\right)$
11 fvres ${⊢}{z}\in \left({X}×{Y}\right)\to \left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)\left({z}\right)={2}^{nd}\left({z}\right)$
12 11 mpteq2ia ${⊢}\left({z}\in \left({X}×{Y}\right)⟼\left({{2}^{nd}↾}_{\left({X}×{Y}\right)}\right)\left({z}\right)\right)=\left({z}\in \left({X}×{Y}\right)⟼{2}^{nd}\left({z}\right)\right)$
13 vex ${⊢}{x}\in \mathrm{V}$
14 vex ${⊢}{y}\in \mathrm{V}$
15 13 14 op2ndd ${⊢}{z}=⟨{x},{y}⟩\to {2}^{nd}\left({z}\right)={y}$
16 15 mpompt ${⊢}\left({z}\in \left({X}×{Y}\right)⟼{2}^{nd}\left({z}\right)\right)=\left({x}\in {X},{y}\in {Y}⟼{y}\right)$
17 10 12 16 3eqtri ${⊢}{{2}^{nd}↾}_{\left({X}×{Y}\right)}=\left({x}\in {X},{y}\in {Y}⟼{y}\right)$
18 tx2cn ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to {{2}^{nd}↾}_{\left({X}×{Y}\right)}\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
19 1 2 18 syl2anc ${⊢}{\phi }\to {{2}^{nd}↾}_{\left({X}×{Y}\right)}\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
20 17 19 eqeltrrid ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{y}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$