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	43	rexeqdv	$⊢ ((((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) \leftrightarrow \exists x \in S x \in g (n))$
45	35 44	mpbird	$⊢ ((((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)$
46	45	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)$
47		fvex	$⊢ I (S) \in V$
48		nnenom	$⊢ ℕ \approx ω$
49		eleq1	$⊢ x = f (n) \to (x \in g (n) \leftrightarrow f (n) \in g (n))$
50	47 48 49	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))$
51	46 50	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))$
52	42	feq3d	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to (f : ℕ ⟶ I (S) \leftrightarrow f : ℕ ⟶ S)$
53	52	biimpd	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land P \in cls (J) (S)) \to (f : ℕ ⟶ I (S) \to f : ℕ ⟶ S)$
54	53	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)$
55	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$
56		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)$
57		eleq2	$⊢ x = y \to (P \in x \leftrightarrow P \in y)$
58		fveq2	$⊢ k = j \to g (k) = g (j)$
59	58	sseq1d	$⊢ k = j \to (g (k) \subseteq x \leftrightarrow g (j) \subseteq x)$
60	59	cbvrexvw	$⊢ \exists k \in ℕ g (k) \subseteq x \leftrightarrow \exists j \in ℕ g (j) \subseteq x$
61		sseq2	$⊢ x = y \to (g (j) \subseteq x \leftrightarrow g (j) \subseteq y)$
62	61	rexbidv	$⊢ x = y \to (\exists j \in ℕ g (j) \subseteq x \leftrightarrow \exists j \in ℕ g (j) \subseteq y)$
63	60 62	bitrid	$⊢ x = y \to (\exists k \in ℕ g (k) \subseteq x \leftrightarrow \exists j \in ℕ g (j) \subseteq y)$
64	57 63	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))$
65	64	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)$
66	56 65	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)$
67		simpr	$⊢ (P \in g (k) \land g (k + 1) \subseteq g (k)) \to g (k + 1) \subseteq g (k)$
68	67	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)$
69	9 68	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)$
70	69	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)$
71		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 ℕ$
72		fveq2	$⊢ n = j \to g (n) = g (j)$
73	72	sseq1d	$⊢ n = j \to (g (n) \subseteq g (j) \leftrightarrow g (j) \subseteq g (j))$
74	73	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)))$
75		fveq2	$⊢ n = m \to g (n) = g (m)$
76	75	sseq1d	$⊢ n = m \to (g (n) \subseteq g (j) \leftrightarrow g (m) \subseteq g (j))$
77	76	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)))$
78		fveq2	$⊢ n = m + 1 \to g (n) = g (m + 1)$
79	78	sseq1d	$⊢ n = m + 1 \to (g (n) \subseteq g (j) \leftrightarrow g (m + 1) \subseteq g (j))$
80	79	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)))$
81		ssid	$⊢ g (j) \subseteq g (j)$
82	81	2a1i	$⊢ j \in ℤ \to ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (j) \subseteq g (j))$
83		eluznn	$⊢ (j \in ℕ \land m \in ℤ_{\geq j}) \to m \in ℕ$
84		fvoveq1	$⊢ k = m \to g (k + 1) = g (m + 1)$
85		fveq2	$⊢ k = m \to g (k) = g (m)$
86	84 85	sseq12d	$⊢ k = m \to (g (k + 1) \subseteq g (k) \leftrightarrow g (m + 1) \subseteq g (m))$
87	86	rspccva	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land m \in ℕ) \to g (m + 1) \subseteq g (m)$
88	83 87	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)$
89	88	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)$
90		sstr2	$⊢ g (m + 1) \subseteq g (m) \to (g (m) \subseteq g (j) \to g (m + 1) \subseteq g (j))$
91	89 90	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))$
92	91	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)))$
93	92	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)))$
94	74 77 80 77 82 93	uzind4	$⊢ m \in ℤ_{\geq j} \to ((\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to g (m) \subseteq g (j))$
95	94	com12	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to (m \in ℤ_{\geq j} \to g (m) \subseteq g (j))$
96	95	ralrimiv	$⊢ (\forall k \in ℕ g (k + 1) \subseteq g (k) \land j \in ℕ) \to \forall m \in ℤ_{\geq j} g (m) \subseteq g (j)$
97	70 71 96	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)$
98		fveq2	$⊢ n = m \to f (n) = f (m)$
99	98 75	eleq12d	$⊢ n = m \to (f (n) \in g (n) \leftrightarrow f (m) \in g (m))$
100		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)$
101	100	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)$
102	71 83	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 ℕ$
103	99 101 102	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)$
104	103	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)$
105		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))$
106	97 104 105	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))$
107		ssel2	$⊢ (g (m) \subseteq g (j) \land f (m) \in g (m)) \to f (m) \in g (j)$
108	107	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)$
109	106 108	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)$
110		ssel	$⊢ g (j) \subseteq y \to (f (m) \in g (j) \to f (m) \in y)$
111	110	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)$
112	109 111	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)$
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	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)$
115	114	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)$
116	66 115	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)$
117	116	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)$
118	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$
119	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
120	118 119	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)$
121		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
122		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 ℤ$
123		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$
124	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$
125	123 124	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$
126		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)$
127	120 121 122 125 126	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)))$
128	55 117 127	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$
129	128	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)$
130	129	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))$
131	54 130	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))$
132	131	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))$
133	51 132	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)$
134	8 133	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)$
135	134	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))$
136	3	ad2antrr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to J \in Top$
137	136 119	sylib	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to J \in TopOn (X)$
138		1zzd	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to 1 \in ℤ$
139		simprr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to f \underset{t}{⇝} (J) P$
140		simprl	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to f : ℕ ⟶ S$
141	140	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$
142		simplr	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to S \subseteq X$
143	121 137 138 139 141 142	lmcls	$⊢ ((J \in 1^{st} 𝜔 \land S \subseteq X) \land (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P)) \to P \in cls (J) (S)$
144	143	ex	$⊢ (J \in 1^{st} 𝜔 \land S \subseteq X) \to ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) P) \to P \in cls (J) (S))$
145	144	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))$
146	135 145	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