1stcelcls

Description: A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of Kreyszig p. 30. This proof uses countable choice ax-cc . A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Hypothesis	1stcelcls.1	$⊢ X = ⋃ J$
	Assertion	1stcelcls	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to (P \in cls (J) (S) \leftrightarrow \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P))$

Proof

Step	Hyp	Ref	Expression
1		1stcelcls.1	$⊢ X = ⋃ J$
2		simpll	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to J \in 1^{st} 𝜔$
3		1stctop	$⊢ J \in 1^{st} 𝜔 \to J \in Top$
4	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
5	3 4	sylan	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to cls (J) (S) \subseteq X$
6	5	sselda	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to P \in X$
7	1	1stcfb	$⊢ (J \in 1^{st} 𝜔 \land P \in X) \to \exists g (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))$
8	2 6 7	syl2anc	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to \exists g (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))$
9		simpr2	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k))$
10		simpl	$⊢ (P \in g (k) \land g (k + 1) \subseteq g (k)) \to P \in g (k)$
11	10	ralimi	$⊢ \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \to \forall k \in ℕ P \in g (k)$
12	9 11	syl	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to \forall k \in ℕ P \in g (k)$
13		fveq2	$⊢ k = n \to g (k) = g (n)$
14	13	eleq2d	$⊢ k = n \to (P \in g (k) \leftrightarrow P \in g (n))$
15	14	rspccva	$⊢ (\forall k \in ℕ P \in g (k) \land n \in ℕ) \to P \in g (n)$
16	12 15	sylan	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to P \in g (n)$
17		eleq2	$⊢ y = g (n) \to (P \in y \leftrightarrow P \in g (n))$
18		ineq1	$⊢ y = g (n) \to y \cap S = g (n) \cap S$
19	18	neeq1d	$⊢ y = g (n) \to (y \cap S \neq \emptyset \leftrightarrow g (n) \cap S \neq \emptyset)$
20	17 19	imbi12d	$⊢ y = g (n) \to ((P \in y \to y \cap S \neq \emptyset) \leftrightarrow (P \in g (n) \to g (n) \cap S \neq \emptyset))$
21	1	elcls2	$⊢ (J \in Top \land S \subseteq X) \to (P \in cls (J) (S) \leftrightarrow (P \in X \land \forall y \in J (P \in y \to y \cap S \neq \emptyset)))$
22	3 21	sylan	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to (P \in cls (J) (S) \leftrightarrow (P \in X \land \forall y \in J (P \in y \to y \cap S \neq \emptyset)))$
23	22	simplbda	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to \forall y \in J (P \in y \to y \cap S \neq \emptyset)$
24	23	ad2antrr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to \forall y \in J (P \in y \to y \cap S \neq \emptyset)$
25		simpr1	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to g : ℕ ⟶ J$
26	25	ffvelcdmda	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to g (n) \in J$
27	20 24 26	rspcdva	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to (P \in g (n) \to g (n) \cap S \neq \emptyset)$
28	16 27	mpd	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to g (n) \cap S \neq \emptyset$
29		elin	$⊢ x \in (g (n) \cap S) \leftrightarrow (x \in g (n) \land x \in S)$
30	29	biancomi	$⊢ x \in (g (n) \cap S) \leftrightarrow (x \in S \land x \in g (n))$
31	30	exbii	$⊢ \exists x x \in (g (n) \cap S) \leftrightarrow \exists x (x \in S \land x \in g (n))$
32		n0	$⊢ g (n) \cap S \neq \emptyset \leftrightarrow \exists x x \in (g (n) \cap S)$
33		df-rex	$⊢ \exists x \in S x \in g (n) \leftrightarrow \exists x (x \in S \land x \in g (n))$
34	31 32 33	3bitr4i	$⊢ g (n) \cap S \neq \emptyset \leftrightarrow \exists x \in S x \in g (n)$
35	28 34	sylib	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to \exists x \in S x \in g (n)$
36	3	ad2antrr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to J \in Top$
37	1	topopn	$⊢ J \in Top \to X \in J$
38	36 37	syl	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to X \in J$
39		simplr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to S \subseteq X$
40	38 39	ssexd	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to S \in V$
41		fvi	$⊢ S \in V \to I (S) = S$
42	40 41	syl	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to I (S) = S$
43	42	ad2antrr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to I (S) = S$
44	35 43	rexeqtrrdv	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land n \in ℕ) \to \exists x \in I (S) x \in g (n)$
45	44	ralrimiva	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to \forall n \in ℕ \exists x \in I (S) x \in g (n)$
46		fvex	$⊢ I (S) \in V$
47		nnenom	$⊢ ℕ \approx ω$
48		eleq1	$⊢ x = f (n) \to (x \in g (n) \leftrightarrow f (n) \in g (n))$
49	46 47 48	axcc4	$⊢ \forall n \in ℕ \exists x \in I (S) x \in g (n) \to \exists f (f : ℕ ⟶ I (S) \land \forall n \in ℕ f (n) \in g (n))$
50	45 49	syl	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to \exists f (f : ℕ ⟶ I (S) \land \forall n \in ℕ f (n) \in g (n))$
51	42	feq3d	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to (f : ℕ ⟶ I (S) \leftrightarrow f : ℕ ⟶ S)$
52	51	biimpd	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to (f : ℕ ⟶ I (S) \to f : ℕ ⟶ S)$
53	52	adantr	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to (f : ℕ ⟶ I (S) \to f : ℕ ⟶ S)$
54	6	ad2antrr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to P \in X$
55		simplr3	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x)$
56		eleq2	$⊢ x = y \to (P \in x \leftrightarrow P \in y)$
57		fveq2	$⊢ k = j \to g (k) = g (j)$
58	57	sseq1d	$⊢ k = j \to (g (k) \subseteq x \leftrightarrow g (j) \subseteq x)$
59	58	cbvrexvw	$⊢ \exists k \in ℕ g (k) \subseteq x \leftrightarrow \exists j \in ℕ g (j) \subseteq x$
60		sseq2	$⊢ x = y \to (g (j) \subseteq x \leftrightarrow g (j) \subseteq y)$
61	60	rexbidv	$⊢ x = y \to (\exists j \in ℕ g (j) \subseteq x \leftrightarrow \exists j \in ℕ g (j) \subseteq y)$
62	59 61	bitrid	$⊢ x = y \to (\exists k \in ℕ g (k) \subseteq x \leftrightarrow \exists j \in ℕ g (j) \subseteq y)$
63	56 62	imbi12d	$⊢ x = y \to ((P \in x \to \exists k \in ℕ g (k) \subseteq x) \leftrightarrow (P \in y \to \exists j \in ℕ g (j) \subseteq y))$
64	63	rspccva	$⊢ (\forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x) \land y \in J) \to (P \in y \to \exists j \in ℕ g (j) \subseteq y)$
65	55 64	sylan	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \land y \in J) \to (P \in y \to \exists j \in ℕ g (j) \subseteq y)$
66		simpr	$⊢ (P \in g (k) \land g (k + 1) \subseteq g (k)) \to g (k + 1) \subseteq g (k)$
67	66	ralimi	$⊢ \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \to \forall k \in ℕ g (k + 1) \subseteq g (k)$
68	9 67	syl	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to \forall k \in ℕ g (k + 1) \subseteq g (k)$
69	68	adantr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to \forall k \in ℕ g (k + 1) \subseteq g (k)$
70		simprrr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to j \in ℕ$
71		fveq2	$⊢ n = j \to g (n) = g (j)$
72	71	sseq1d	$⊢ n = j \to (g (n) \subseteq g (j) \leftrightarrow g (j) \subseteq g (j))$
73	72	imbi2d	$⊢ n = j \to (((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (n) \subseteq g (j)) \leftrightarrow ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (j) \subseteq g (j)))$
74		fveq2	$⊢ n = m \to g (n) = g (m)$
75	74	sseq1d	$⊢ n = m \to (g (n) \subseteq g (j) \leftrightarrow g (m) \subseteq g (j))$
76	75	imbi2d	$⊢ n = m \to (((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (n) \subseteq g (j)) \leftrightarrow ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (m) \subseteq g (j)))$
77		fveq2	$⊢ n = m + 1 \to g (n) = g (m + 1)$
78	77	sseq1d	$⊢ n = m + 1 \to (g (n) \subseteq g (j) \leftrightarrow g (m + 1) \subseteq g (j))$
79	78	imbi2d	$⊢ n = m + 1 \to (((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (n) \subseteq g (j)) \leftrightarrow ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (m + 1) \subseteq g (j)))$
80		ssid	$⊢ g (j) \subseteq g (j)$
81	80	2a1i	$⊢ j \in ℤ \to ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (j) \subseteq g (j))$
82		eluznn	$⊢ (j \in ℕ \land m \in ℤ_{\geq j}) \to m \in ℕ$
83		fvoveq1	$⊢ k = m \to g (k + 1) = g (m + 1)$
84		fveq2	$⊢ k = m \to g (k) = g (m)$
85	83 84	sseq12d	$⊢ k = m \to (g (k + 1) \subseteq g (k) \leftrightarrow g (m + 1) \subseteq g (m))$
86	85	rspccva	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land m \in ℕ) \to g (m + 1) \subseteq g (m)$
87	82 86	sylan2	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land (j \in ℕ \land m \in ℤ_{\geq j})) \to g (m + 1) \subseteq g (m)$
88	87	anassrs	$⊢ ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \land m \in ℤ_{\geq j}) \to g (m + 1) \subseteq g (m)$
89		sstr2	$⊢ g (m + 1) \subseteq g (m) \to (g (m) \subseteq g (j) \to g (m + 1) \subseteq g (j))$
90	88 89	syl	$⊢ ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \land m \in ℤ_{\geq j}) \to (g (m) \subseteq g (j) \to g (m + 1) \subseteq g (j))$
91	90	expcom	$⊢ m \in ℤ_{\geq j} \to ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to (g (m) \subseteq g (j) \to g (m + 1) \subseteq g (j)))$
92	91	a2d	$⊢ m \in ℤ_{\geq j} \to (((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (m) \subseteq g (j)) \to ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (m + 1) \subseteq g (j)))$
93	73 76 79 76 81 92	uzind4	$⊢ m \in ℤ_{\geq j} \to ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (m) \subseteq g (j))$
94	93	com12	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to (m \in ℤ_{\geq j} \to g (m) \subseteq g (j))$
95	94	ralrimiv	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to \forall m \in ℤ_{\geq j} g (m) \subseteq g (j)$
96	69 70 95	syl2anc	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to \forall m \in ℤ_{\geq j} g (m) \subseteq g (j)$
97		fveq2	$⊢ n = m \to f (n) = f (m)$
98	97 74	eleq12d	$⊢ n = m \to (f (n) \in g (n) \leftrightarrow f (m) \in g (m))$
99		simplr	$⊢ ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ)) \to \forall n \in ℕ f (n) \in g (n)$
100	99	ad2antlr	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \land m \in ℤ_{\geq j}) \to \forall n \in ℕ f (n) \in g (n)$
101	70 82	sylan	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \land m \in ℤ_{\geq j}) \to m \in ℕ$
102	98 100 101	rspcdva	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \land m \in ℤ_{\geq j}) \to f (m) \in g (m)$
103	102	ralrimiva	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to \forall m \in ℤ_{\geq j} f (m) \in g (m)$
104		r19.26	$⊢ \forall m \in ℤ_{\geq j} (g (m) \subseteq g (j) \land f (m) \in g (m)) \leftrightarrow (\forall m \in ℤ_{\geq j} g (m) \subseteq g (j) \land \forall m \in ℤ_{\geq j} f (m) \in g (m))$
105	96 103 104	sylanbrc	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to \forall m \in ℤ_{\geq j} (g (m) \subseteq g (j) \land f (m) \in g (m))$
106		ssel2	$⊢ (g (m) \subseteq g (j) \land f (m) \in g (m)) \to f (m) \in g (j)$
107	106	ralimi	$⊢ \forall m \in ℤ_{\geq j} (g (m) \subseteq g (j) \land f (m) \in g (m)) \to \forall m \in ℤ_{\geq j} f (m) \in g (j)$
108	105 107	syl	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to \forall m \in ℤ_{\geq j} f (m) \in g (j)$
109		ssel	$⊢ g (j) \subseteq y \to (f (m) \in g (j) \to f (m) \in y)$
110	109	ralimdv	$⊢ g (j) \subseteq y \to (\forall m \in ℤ_{\geq j} f (m) \in g (j) \to \forall m \in ℤ_{\geq j} f (m) \in y)$
111	108 110	syl5com	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \land (y \in J \land j \in ℕ))) \to (g (j) \subseteq y \to \forall m \in ℤ_{\geq j} f (m) \in y)$
112	111	anassrs	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \land (y \in J \land j \in ℕ)) \to (g (j) \subseteq y \to \forall m \in ℤ_{\geq j} f (m) \in y)$
113	112	anassrs	$⊢ ((((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \land y \in J) \land j \in ℕ) \to (g (j) \subseteq y \to \forall m \in ℤ_{\geq j} f (m) \in y)$
114	113	reximdva	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \land y \in J) \to (\exists j \in ℕ g (j) \subseteq y \to \exists j \in ℕ \forall m \in ℤ_{\geq j} f (m) \in y)$
115	65 114	syld	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \land y \in J) \to (P \in y \to \exists j \in ℕ \forall m \in ℤ_{\geq j} f (m) \in y)$
116	115	ralrimiva	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to \forall y \in J (P \in y \to \exists j \in ℕ \forall m \in ℤ_{\geq j} f (m) \in y)$
117	36	ad2antrr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to J \in Top$
118	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
119	117 118	sylib	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to J \in TopOn (X)$
120		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
121		1zzd	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to 1 \in ℤ$
122		simprl	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to f : ℕ ⟶ S$
123	39	ad2antrr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to S \subseteq X$
124	122 123	fssd	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to f : ℕ ⟶ X$
125		eqidd	$⊢ (((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \land m \in ℕ) \to f (m) = f (m)$
126	119 120 121 124 125	lmbrf	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to (f \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall y \in J (P \in y \to \exists j \in ℕ \forall m \in ℤ_{\geq j} f (m) \in y)))$
127	54 116 126	mpbir2and	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land (f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n))) \to f \underset{t}{⇝} (J) P$
128	127	expr	$⊢ ((((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \land f : ℕ ⟶ S) \to (\forall n \in ℕ f (n) \in g (n) \to f \underset{t}{⇝} (J) P)$
129	128	imdistanda	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to ((f : ℕ ⟶ S \land \forall n \in ℕ f (n) \in g (n)) \to (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P))$
130	53 129	syland	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to ((f : ℕ ⟶ I (S) \land \forall n \in ℕ f (n) \in g (n)) \to (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P))$
131	130	eximdv	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to (\exists f (f : ℕ ⟶ I (S) \land \forall n \in ℕ f (n) \in g (n)) \to \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P))$
132	50 131	mpd	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \land (g : ℕ ⟶ J \land \forall k \in ℕ (P \in g (k) \land g (k + 1) \subseteq g (k)) \land \forall x \in J (P \in x \to \exists k \in ℕ g (k) \subseteq x))) \to \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)$
133	8 132	exlimddv	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)$
134	133	ex	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to (P \in cls (J) (S) \to \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P))$
135	3	ad2antrr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to J \in Top$
136	135 118	sylib	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to J \in TopOn (X)$
137		1zzd	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to 1 \in ℤ$
138		simprr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to f \underset{t}{⇝} (J) P$
139		simprl	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to f : ℕ ⟶ S$
140	139	ffvelcdmda	$⊢ (((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \land k \in ℕ) \to f (k) \in S$
141		simplr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to S \subseteq X$
142	120 136 137 138 140 141	lmcls	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to P \in cls (J) (S)$
143	142	ex	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P) \to P \in cls (J) (S))$
144	143	exlimdv	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to (\exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P) \to P \in cls (J) (S))$
145	134 144	impbid	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to (P \in cls (J) (S) \leftrightarrow \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P))$

Metamath Proof Explorer

Theorem 1stcelcls

Proof