Theorem 1stccn

Description: A mapping X --> Y , where X is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence f ( n ) converging to x , its image under F converges to F ( x ) . (Contributed by Mario Carneiro, 7-Sep-2015)

	Ref	Expression
Hypotheses	1stccnp.1	$$⊢\phi \to J\in 1^{st}𝜔$$
	1stccnp.2	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	1stccnp.3	$$⊢\phi \to K\in \mathrm{TopOn}\left(Y\right)$$
	1stccn.7	$$⊢\phi \to F:X⟶Y$$
Assertion	1stccn	$$⊢\phi \to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1stccnp.1	$$⊢\phi \to J\in 1^{st}𝜔$$
2		1stccnp.2	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
3		1stccnp.3	$$⊢\phi \to K\in \mathrm{TopOn}\left(Y\right)$$
4		1stccn.7	$$⊢\phi \to F:X⟶Y$$
5		cncnp	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge K\in \mathrm{TopOn}\left(Y\right)\right)\to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \left(F:X⟶Y\wedge \forall x\in XF\in \left(J\mathrm{CnP}K\right)\left(x\right)\right)\right)$$
6	2 3 5	syl2anc	$$⊢\phi \to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \left(F:X⟶Y\wedge \forall x\in XF\in \left(J\mathrm{CnP}K\right)\left(x\right)\right)\right)$$
7	4 6	mpbirand	$$⊢\phi \to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \forall x\in XF\in \left(J\mathrm{CnP}K\right)\left(x\right)\right)$$
8	4	adantr	$$⊢\left(\phi \wedge x\in X\right)\to F:X⟶Y$$
9	1	adantr	$$⊢\left(\phi \wedge x\in X\right)\to J\in 1^{st}𝜔$$
10	2	adantr	$$⊢\left(\phi \wedge x\in X\right)\to J\in \mathrm{TopOn}\left(X\right)$$
11	3	adantr	$$⊢\left(\phi \wedge x\in X\right)\to K\in \mathrm{TopOn}\left(Y\right)$$
12		simpr	$$⊢\left(\phi \wedge x\in X\right)\to x\in X$$
13	9 10 11 12	1stccnp	$$⊢\left(\phi \wedge x\in X\right)\to \left(F\in \left(J\mathrm{CnP}K\right)\left(x\right)\leftrightarrow \left(F:X⟶Y\wedge \forall f\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$
14	8 13	mpbirand	$$⊢\left(\phi \wedge x\in X\right)\to \left(F\in \left(J\mathrm{CnP}K\right)\left(x\right)\leftrightarrow \forall f\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
15	14	ralbidva	$$⊢\phi \to \left(\forall x\in XF\in \left(J\mathrm{CnP}K\right)\left(x\right)\leftrightarrow \forall x\in X\forall f\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
16		ralcom4	$$⊢\forall x\in X\forall f\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \forall f\forall x\in X\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)$$
17		impexp	$$⊢\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
18	17	ralbii	$$⊢\forall x\in X\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \forall x\in X\left(f:\mathbb{N}⟶X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
19		r19.21v	$$⊢\forall x\in X\left(f:\mathbb{N}⟶X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \forall x\in X\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
20	18 19	bitri	$$⊢\forall x\in X\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \forall x\in X\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
21		df-ral	$$⊢\forall x\in X\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \forall x\left(x\in X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
22		lmcl	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge f\underset{t}{⇝}\left(J\right)x\right)\to x\in X$$
23	2 22	sylan	$$⊢\left(\phi \wedge f\underset{t}{⇝}\left(J\right)x\right)\to x\in X$$
24	23	ex	$$⊢\phi \to \left(f\underset{t}{⇝}\left(J\right)x\to x\in X\right)$$
25	24	pm4.71rd	$$⊢\phi \to \left(f\underset{t}{⇝}\left(J\right)x\leftrightarrow \left(x\in X\wedge f\underset{t}{⇝}\left(J\right)x\right)\right)$$
26	25	imbi1d	$$⊢\phi \to \left(\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \left(\left(x\in X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
27		impexp	$$⊢\left(\left(x\in X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \left(x\in X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
28	26 27	bitr2di	$$⊢\phi \to \left(\left(x\in X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\leftrightarrow \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
29	28	albidv	$$⊢\phi \to \left(\forall x\left(x\in X\to \left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\leftrightarrow \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
30	21 29	bitrid	$$⊢\phi \to \left(\forall x\in X\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)$$
31	30	imbi2d	$$⊢\phi \to \left(\left(f:\mathbb{N}⟶X\to \forall x\in X\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$
32	20 31	bitrid	$$⊢\phi \to \left(\forall x\in X\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$
33	32	albidv	$$⊢\phi \to \left(\forall f\forall x\in X\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$
34	16 33	bitrid	$$⊢\phi \to \left(\forall x\in X\forall f\left(\left(f:\mathbb{N}⟶X\wedge f\underset{t}{⇝}\left(J\right)x\right)\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$
35	7 15 34	3bitrd	$$⊢\phi \to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$