1stccnp

Description: A mapping is continuous at P in a first-countable space X iff it is sequentially continuous at P , meaning that the image under F of every sequence converging at P converges to F ( P ) . This proof uses ax-cc , but only via 1stcelcls , so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015)

	Ref	Expression
Hypotheses	1stccnp.1	$⊢ φ \to J \in 1^{st} 𝜔$
	1stccnp.2	$⊢ φ \to J \in TopOn (X)$
	1stccnp.3	$⊢ φ \to K \in TopOn (Y)$
	1stccnp.4	$⊢ φ \to P \in X$
Assertion	1stccnp	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P))))$

Proof

Step	Hyp	Ref	Expression
1		1stccnp.1	$⊢ φ \to J \in 1^{st} 𝜔$
2		1stccnp.2	$⊢ φ \to J \in TopOn (X)$
3		1stccnp.3	$⊢ φ \to K \in TopOn (Y)$
4		1stccnp.4	$⊢ φ \to P \in X$
5	2 3	jca	$⊢ φ \to (J \in TopOn (X) \land K \in TopOn (Y))$
6		cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
7	6	3expa	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
8	5 7	sylan	$⊢ (φ \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
9		simprr	$⊢ ((φ \land F \in (J CnP K) (P)) \land (f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P)) \to f \underset{t}{⇝} (J) P$
10		simplr	$⊢ ((φ \land F \in (J CnP K) (P)) \land (f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P)) \to F \in (J CnP K) (P)$
11	9 10	lmcnp	$⊢ ((φ \land F \in (J CnP K) (P)) \land (f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P)) \to (F \circ f) \underset{t}{⇝} (K) F (P)$
12	11	ex	$⊢ (φ \land F \in (J CnP K) (P)) \to ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P))$
13	12	alrimiv	$⊢ (φ \land F \in (J CnP K) (P)) \to \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P))$
14	8 13	jca	$⊢ (φ \land F \in (J CnP K) (P)) \to (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))$
15		simprl	$⊢ (φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \to F : X ⟶ Y$
16		fal	$⊢ \neg ⊥$
17		19.29	$⊢ (\forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \land \exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to \exists f (((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P))$
18		simprl	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to f : ℕ ⟶ X ∖ F^{-1} [u]$
19		difss	$⊢ X ∖ F^{-1} [u] \subseteq X$
20		fss	$⊢ (f : ℕ ⟶ X ∖ F^{-1} [u] \land X ∖ F^{-1} [u] \subseteq X) \to f : ℕ ⟶ X$
21	18 19 20	sylancl	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to f : ℕ ⟶ X$
22		simprr	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to f \underset{t}{⇝} (J) P$
23	21 22	jca	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to (f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P)$
24		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
25		simplrr	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to F (P) \in u$
26		1zzd	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to 1 \in ℤ$
27		simprr	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to (F \circ f) \underset{t}{⇝} (K) F (P)$
28		simplrl	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to u \in K$
29	24 25 26 27 28	lmcvg	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (F \circ f) (k) \in u$
30	24	r19.2uz	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} (F \circ f) (k) \in u \to \exists k \in ℕ (F \circ f) (k) \in u$
31		simprll	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to f : ℕ ⟶ X ∖ F^{-1} [u]$
32	31	ffnd	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to f Fn ℕ$
33		fvco2	$⊢ (f Fn ℕ \land k \in ℕ) \to (F \circ f) (k) = F (f (k))$
34	32 33	sylan	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to (F \circ f) (k) = F (f (k))$
35	34	eleq1d	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to ((F \circ f) (k) \in u \leftrightarrow F (f (k)) \in u)$
36	31	ffvelrnda	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to f (k) \in (X ∖ F^{-1} [u])$
37	36	eldifad	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to f (k) \in X$
38		simplr	$⊢ ((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \to F : X ⟶ Y$
39	38	ad2antrr	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to F : X ⟶ Y$
40		ffn	$⊢ F : X ⟶ Y \to F Fn X$
41		elpreima	$⊢ F Fn X \to (f (k) \in F^{-1} [u] \leftrightarrow (f (k) \in X \land F (f (k)) \in u))$
42	39 40 41	3syl	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to (f (k) \in F^{-1} [u] \leftrightarrow (f (k) \in X \land F (f (k)) \in u))$
43	36	eldifbd	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to \neg f (k) \in F^{-1} [u]$
44	43	pm2.21d	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to (f (k) \in F^{-1} [u] \to ⊥)$
45	42 44	sylbird	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to ((f (k) \in X \land F (f (k)) \in u) \to ⊥)$
46	37 45	mpand	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to (F (f (k)) \in u \to ⊥)$
47	35 46	sylbid	$⊢ ((((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \land k \in ℕ) \to ((F \circ f) (k) \in u \to ⊥)$
48	47	rexlimdva	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to (\exists k \in ℕ (F \circ f) (k) \in u \to ⊥)$
49	30 48	syl5	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (F \circ f) (k) \in u \to ⊥)$
50	29 49	mpd	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \land (F \circ f) \underset{t}{⇝} (K) F (P))) \to ⊥$
51	50	expr	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to ((F \circ f) \underset{t}{⇝} (K) F (P) \to ⊥)$
52	23 51	embantd	$⊢ (((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to (((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \to ⊥)$
53	52	ex	$⊢ ((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \to ((f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \to (((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \to ⊥))$
54	53	impcomd	$⊢ ((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \to ((((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to ⊥)$
55	54	exlimdv	$⊢ ((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \to (\exists f (((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \land (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to ⊥)$
56	17 55	syl5	$⊢ ((φ \land F : X ⟶ Y) \land (u \in K \land F (P) \in u)) \to ((\forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \land \exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)) \to ⊥)$
57	56	exp4b	$⊢ (φ \land F : X ⟶ Y) \to ((u \in K \land F (P) \in u) \to (\forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \to (\exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \to ⊥)))$
58	57	com23	$⊢ (φ \land F : X ⟶ Y) \to (\forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)) \to ((u \in K \land F (P) \in u) \to (\exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \to ⊥)))$
59	58	impr	$⊢ (φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \to ((u \in K \land F (P) \in u) \to (\exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \to ⊥))$
60	59	imp	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to (\exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P) \to ⊥)$
61	16 60	mtoi	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to \neg \exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P)$
62	1	ad2antrr	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to J \in 1^{st} 𝜔$
63	2	ad2antrr	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to J \in TopOn (X)$
64		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
65	63 64	syl	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to X = ⋃ J$
66	19 65	sseqtrid	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to X ∖ F^{-1} [u] \subseteq ⋃ J$
67		eqid	$⊢ ⋃ J = ⋃ J$
68	67	1stcelcls	$⊢ (J \in 1^{st} 𝜔 \land X ∖ F^{-1} [u] \subseteq ⋃ J) \to (P \in cls (J) (X ∖ F^{-1} [u]) \leftrightarrow \exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P))$
69	62 66 68	syl2anc	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to (P \in cls (J) (X ∖ F^{-1} [u]) \leftrightarrow \exists f (f : ℕ ⟶ X ∖ F^{-1} [u] \land f \underset{t}{⇝} (J) P))$
70	61 69	mtbird	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to \neg P \in cls (J) (X ∖ F^{-1} [u])$
71		topontop	$⊢ J \in TopOn (X) \to J \in Top$
72	63 71	syl	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to J \in Top$
73	4	ad2antrr	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to P \in X$
74	73 65	eleqtrd	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to P \in ⋃ J$
75	67	elcls	$⊢ (J \in Top \land X ∖ F^{-1} [u] \subseteq ⋃ J \land P \in ⋃ J) \to (P \in cls (J) (X ∖ F^{-1} [u]) \leftrightarrow \forall v \in J (P \in v \to v \cap (X ∖ F^{-1} [u]) \neq \emptyset))$
76	72 66 74 75	syl3anc	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to (P \in cls (J) (X ∖ F^{-1} [u]) \leftrightarrow \forall v \in J (P \in v \to v \cap (X ∖ F^{-1} [u]) \neq \emptyset))$
77	70 76	mtbid	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to \neg \forall v \in J (P \in v \to v \cap (X ∖ F^{-1} [u]) \neq \emptyset)$
78	15	ad2antrr	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to F : X ⟶ Y$
79	78	ffund	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to Fun F$
80		toponss	$⊢ (J \in TopOn (X) \land v \in J) \to v \subseteq X$
81	63 80	sylan	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to v \subseteq X$
82	78	fdmd	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to dom F = X$
83	81 82	sseqtrrd	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to v \subseteq dom F$
84		funimass3	$⊢ (Fun F \land v \subseteq dom F) \to (F [v] \subseteq u \leftrightarrow v \subseteq F^{-1} [u])$
85	79 83 84	syl2anc	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to (F [v] \subseteq u \leftrightarrow v \subseteq F^{-1} [u])$
86		df-ss	$⊢ v \subseteq X \leftrightarrow v \cap X = v$
87	81 86	sylib	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to v \cap X = v$
88	87	sseq1d	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to (v \cap X \subseteq F^{-1} [u] \leftrightarrow v \subseteq F^{-1} [u])$
89	85 88	bitr4d	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to (F [v] \subseteq u \leftrightarrow v \cap X \subseteq F^{-1} [u])$
90		nne	$⊢ \neg v \cap (X ∖ F^{-1} [u]) \neq \emptyset \leftrightarrow v \cap (X ∖ F^{-1} [u]) = \emptyset$
91		inssdif0	$⊢ v \cap X \subseteq F^{-1} [u] \leftrightarrow v \cap (X ∖ F^{-1} [u]) = \emptyset$
92	90 91	bitr4i	$⊢ \neg v \cap (X ∖ F^{-1} [u]) \neq \emptyset \leftrightarrow v \cap X \subseteq F^{-1} [u]$
93	89 92	bitr4di	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to (F [v] \subseteq u \leftrightarrow \neg v \cap (X ∖ F^{-1} [u]) \neq \emptyset)$
94	93	anbi2d	$⊢ (((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \land v \in J) \to ((P \in v \land F [v] \subseteq u) \leftrightarrow (P \in v \land \neg v \cap (X ∖ F^{-1} [u]) \neq \emptyset))$
95	94	rexbidva	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to (\exists v \in J (P \in v \land F [v] \subseteq u) \leftrightarrow \exists v \in J (P \in v \land \neg v \cap (X ∖ F^{-1} [u]) \neq \emptyset))$
96		rexanali	$⊢ \exists v \in J (P \in v \land \neg v \cap (X ∖ F^{-1} [u]) \neq \emptyset) \leftrightarrow \neg \forall v \in J (P \in v \to v \cap (X ∖ F^{-1} [u]) \neq \emptyset)$
97	95 96	bitrdi	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to (\exists v \in J (P \in v \land F [v] \subseteq u) \leftrightarrow \neg \forall v \in J (P \in v \to v \cap (X ∖ F^{-1} [u]) \neq \emptyset))$
98	77 97	mpbird	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land (u \in K \land F (P) \in u)) \to \exists v \in J (P \in v \land F [v] \subseteq u)$
99	98	expr	$⊢ ((φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \land u \in K) \to (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))$
100	99	ralrimiva	$⊢ (φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \to \forall u \in K (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))$
101		iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall u \in K (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))))$
102	2 3 4 101	syl3anc	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall u \in K (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))))$
103	102	adantr	$⊢ (φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall u \in K (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))))$
104	15 100 103	mpbir2and	$⊢ (φ \land (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P)))) \to F \in (J CnP K) (P)$
105	14 104	impbida	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P))))$

Metamath Proof Explorer

Theorem 1stccnp

Proof