1stcfb

Description: For any point A in a first-countable topology, there is a function f : NN --> J enumerating neighborhoods of A which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Hypothesis	1stcclb.1	$⊢ X = ⋃ J$
	Assertion	1stcfb	$⊢ (J \in 1^{st} 𝜔 \land A \in X) \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y))$

Proof

Step	Hyp	Ref	Expression
1		1stcclb.1	$⊢ X = ⋃ J$
2	1	1stcclb	$⊢ (J \in 1^{st} 𝜔 \land A \in X) \to \exists x \in 𝒫 J (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z)))$
3		simplr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to A \in X$
4		eleq2	$⊢ z = X \to (A \in z \leftrightarrow A \in X)$
5		sseq2	$⊢ z = X \to (w \subseteq z \leftrightarrow w \subseteq X)$
6	5	anbi2d	$⊢ z = X \to ((A \in w \land w \subseteq z) \leftrightarrow (A \in w \land w \subseteq X))$
7	6	rexbidv	$⊢ z = X \to (\exists w \in x (A \in w \land w \subseteq z) \leftrightarrow \exists w \in x (A \in w \land w \subseteq X))$
8	4 7	imbi12d	$⊢ z = X \to ((A \in z \to \exists w \in x (A \in w \land w \subseteq z)) \leftrightarrow (A \in X \to \exists w \in x (A \in w \land w \subseteq X)))$
9		simprrr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))$
10		1stctop	$⊢ J \in 1^{st} 𝜔 \to J \in Top$
11	10	ad2antrr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to J \in Top$
12	1	topopn	$⊢ J \in Top \to X \in J$
13	11 12	syl	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to X \in J$
14	8 9 13	rspcdva	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to (A \in X \to \exists w \in x (A \in w \land w \subseteq X))$
15	3 14	mpd	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \exists w \in x (A \in w \land w \subseteq X)$
16		simpl	$⊢ (A \in w \land w \subseteq X) \to A \in w$
17	16	reximi	$⊢ \exists w \in x (A \in w \land w \subseteq X) \to \exists w \in x A \in w$
18	15 17	syl	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \exists w \in x A \in w$
19		eleq2w	$⊢ w = a \to (A \in w \leftrightarrow A \in a)$
20	19	cbvrexvw	$⊢ \exists w \in x A \in w \leftrightarrow \exists a \in x A \in a$
21	18 20	sylib	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \exists a \in x A \in a$
22		rabn0	$⊢ \{a \in x \| A \in a\} \neq \emptyset \leftrightarrow \exists a \in x A \in a$
23	21 22	sylibr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \{a \in x \| A \in a\} \neq \emptyset$
24		vex	$⊢ x \in V$
25	24	rabex	$⊢ \{a \in x \| A \in a\} \in V$
26	25	0sdom	$⊢ \emptyset ≺ \{a \in x \| A \in a\} \leftrightarrow \{a \in x \| A \in a\} \neq \emptyset$
27	23 26	sylibr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \emptyset ≺ \{a \in x \| A \in a\}$
28		ssrab2	$⊢ \{a \in x \| A \in a\} \subseteq x$
29		ssdomg	$⊢ x \in V \to (\{a \in x \| A \in a\} \subseteq x \to \{a \in x \| A \in a\} ≼ x)$
30	24 28 29	mp2	$⊢ \{a \in x \| A \in a\} ≼ x$
31		simprrl	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to x ≼ ω$
32		nnenom	$⊢ ℕ \approx ω$
33	32	ensymi	$⊢ ω \approx ℕ$
34		domentr	$⊢ (x ≼ ω \land ω \approx ℕ) \to x ≼ ℕ$
35	31 33 34	sylancl	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to x ≼ ℕ$
36		domtr	$⊢ (\{a \in x \| A \in a\} ≼ x \land x ≼ ℕ) \to \{a \in x \| A \in a\} ≼ ℕ$
37	30 35 36	sylancr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \{a \in x \| A \in a\} ≼ ℕ$
38		fodomr	$⊢ (\emptyset ≺ \{a \in x \| A \in a\} \land \{a \in x \| A \in a\} ≼ ℕ) \to \exists g g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\}$
39	27 37 38	syl2anc	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \exists g g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\}$
40	10	ad3antrrr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to J \in Top$
41		imassrn	$⊢ g [(1 \dots n)] \subseteq ran g$
42		forn	$⊢ g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\} \to ran g = \{a \in x \| A \in a\}$
43	42	ad2antll	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to ran g = \{a \in x \| A \in a\}$
44		simprll	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to x \in 𝒫 J$
45	44	elpwid	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to x \subseteq J$
46	28 45	sstrid	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to \{a \in x \| A \in a\} \subseteq J$
47	43 46	eqsstrd	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to ran g \subseteq J$
48	47	adantr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to ran g \subseteq J$
49	41 48	sstrid	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to g [(1 \dots n)] \subseteq J$
50		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
51		fof	$⊢ g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\} \to g : ℕ ⟶ \{a \in x \| A \in a\}$
52	51	ad2antll	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to g : ℕ ⟶ \{a \in x \| A \in a\}$
53	52	fdmd	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to dom g = ℕ$
54	50 53	sseqtrrid	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to (1 \dots n) \subseteq dom g$
55	54	adantr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to (1 \dots n) \subseteq dom g$
56		sseqin2	$⊢ (1 \dots n) \subseteq dom g \leftrightarrow dom g \cap (1 \dots n) = (1 \dots n)$
57	55 56	sylib	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to dom g \cap (1 \dots n) = (1 \dots n)$
58		elfz1end	$⊢ n \in ℕ \leftrightarrow n \in (1 \dots n)$
59		ne0i	$⊢ n \in (1 \dots n) \to (1 \dots n) \neq \emptyset$
60	59	adantl	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in (1 \dots n)) \to (1 \dots n) \neq \emptyset$
61	58 60	sylan2b	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to (1 \dots n) \neq \emptyset$
62	57 61	eqnetrd	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to dom g \cap (1 \dots n) \neq \emptyset$
63		imadisj	$⊢ g [(1 \dots n)] = \emptyset \leftrightarrow dom g \cap (1 \dots n) = \emptyset$
64	63	necon3bii	$⊢ g [(1 \dots n)] \neq \emptyset \leftrightarrow dom g \cap (1 \dots n) \neq \emptyset$
65	62 64	sylibr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to g [(1 \dots n)] \neq \emptyset$
66		fzfid	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to (1 \dots n) \in Fin$
67	52	ffund	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to Fun g$
68		fores	$⊢ (Fun g \land (1 \dots n) \subseteq dom g) \to ({g ↾}_{(1 \dots n)}) : (1 \dots n) \underset{onto}{⟶} g [(1 \dots n)]$
69	67 55 68	syl2an2r	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to ({g ↾}_{(1 \dots n)}) : (1 \dots n) \underset{onto}{⟶} g [(1 \dots n)]$
70		fofi	$⊢ ((1 \dots n) \in Fin \land ({g ↾}_{(1 \dots n)}) : (1 \dots n) \underset{onto}{⟶} g [(1 \dots n)]) \to g [(1 \dots n)] \in Fin$
71	66 69 70	syl2anc	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to g [(1 \dots n)] \in Fin$
72		fiinopn	$⊢ J \in Top \to ((g [(1 \dots n)] \subseteq J \land g [(1 \dots n)] \neq \emptyset \land g [(1 \dots n)] \in Fin) \to ⋂ g [(1 \dots n)] \in J)$
73	72	imp	$⊢ (J \in Top \land (g [(1 \dots n)] \subseteq J \land g [(1 \dots n)] \neq \emptyset \land g [(1 \dots n)] \in Fin)) \to ⋂ g [(1 \dots n)] \in J$
74	40 49 65 71 73	syl13anc	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land n \in ℕ) \to ⋂ g [(1 \dots n)] \in J$
75	74	fmpttd	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) : ℕ ⟶ J$
76		imassrn	$⊢ g [(1 \dots k)] \subseteq ran g$
77	43	adantr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to ran g = \{a \in x \| A \in a\}$
78	76 77	sseqtrid	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to g [(1 \dots k)] \subseteq \{a \in x \| A \in a\}$
79		id	$⊢ A \in n \to A \in n$
80	79	rgenw	$⊢ \forall n \in x (A \in n \to A \in n)$
81		eleq2w	$⊢ a = n \to (A \in a \leftrightarrow A \in n)$
82	81	ralrab	$⊢ \forall n \in \{a \in x \| A \in a\} A \in n \leftrightarrow \forall n \in x (A \in n \to A \in n)$
83	80 82	mpbir	$⊢ \forall n \in \{a \in x \| A \in a\} A \in n$
84		ssralv	$⊢ g [(1 \dots k)] \subseteq \{a \in x \| A \in a\} \to (\forall n \in \{a \in x \| A \in a\} A \in n \to \forall n \in g [(1 \dots k)] A \in n)$
85	78 83 84	mpisyl	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to \forall n \in g [(1 \dots k)] A \in n$
86		elintg	$⊢ A \in X \to (A \in ⋂ g [(1 \dots k)] \leftrightarrow \forall n \in g [(1 \dots k)] A \in n)$
87	86	ad3antlr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to (A \in ⋂ g [(1 \dots k)] \leftrightarrow \forall n \in g [(1 \dots k)] A \in n)$
88	85 87	mpbird	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to A \in ⋂ g [(1 \dots k)]$
89		eqid	$⊢ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) = (n \in ℕ ⟼ ⋂ g [(1 \dots n)])$
90		oveq2	$⊢ n = k \to (1 \dots n) = (1 \dots k)$
91	90	imaeq2d	$⊢ n = k \to g [(1 \dots n)] = g [(1 \dots k)]$
92	91	inteqd	$⊢ n = k \to ⋂ g [(1 \dots n)] = ⋂ g [(1 \dots k)]$
93		simpr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to k \in ℕ$
94	74	ralrimiva	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to \forall n \in ℕ ⋂ g [(1 \dots n)] \in J$
95	92	eleq1d	$⊢ n = k \to (⋂ g [(1 \dots n)] \in J \leftrightarrow ⋂ g [(1 \dots k)] \in J)$
96	95	rspccva	$⊢ (\forall n \in ℕ ⋂ g [(1 \dots n)] \in J \land k \in ℕ) \to ⋂ g [(1 \dots k)] \in J$
97	94 96	sylan	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to ⋂ g [(1 \dots k)] \in J$
98	89 92 93 97	fvmptd3	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) = ⋂ g [(1 \dots k)]$
99	88 98	eleqtrrd	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)$
100		fzssp1	$⊢ (1 \dots k) \subseteq (1 \dots k + 1)$
101		imass2	$⊢ (1 \dots k) \subseteq (1 \dots k + 1) \to g [(1 \dots k)] \subseteq g [(1 \dots k + 1)]$
102	100 101	mp1i	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to g [(1 \dots k)] \subseteq g [(1 \dots k + 1)]$
103		intss	$⊢ g [(1 \dots k)] \subseteq g [(1 \dots k + 1)] \to ⋂ g [(1 \dots k + 1)] \subseteq ⋂ g [(1 \dots k)]$
104	102 103	syl	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to ⋂ g [(1 \dots k + 1)] \subseteq ⋂ g [(1 \dots k)]$
105		oveq2	$⊢ n = k + 1 \to (1 \dots n) = (1 \dots k + 1)$
106	105	imaeq2d	$⊢ n = k + 1 \to g [(1 \dots n)] = g [(1 \dots k + 1)]$
107	106	inteqd	$⊢ n = k + 1 \to ⋂ g [(1 \dots n)] = ⋂ g [(1 \dots k + 1)]$
108		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
109	108	adantl	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to k + 1 \in ℕ$
110	107	eleq1d	$⊢ n = k + 1 \to (⋂ g [(1 \dots n)] \in J \leftrightarrow ⋂ g [(1 \dots k + 1)] \in J)$
111	110	rspccva	$⊢ (\forall n \in ℕ ⋂ g [(1 \dots n)] \in J \land k + 1 \in ℕ) \to ⋂ g [(1 \dots k + 1)] \in J$
112	94 108 111	syl2an	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to ⋂ g [(1 \dots k + 1)] \in J$
113	89 107 109 112	fvmptd3	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) = ⋂ g [(1 \dots k + 1)]$
114	104 113 98	3sstr4d	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)$
115	99 114	jca	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to (A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \land (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k))$
116	115	ralrimiva	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to \forall k \in ℕ (A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \land (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k))$
117		simprlr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))$
118		eleq2w	$⊢ z = y \to (A \in z \leftrightarrow A \in y)$
119		sseq2	$⊢ z = y \to (w \subseteq z \leftrightarrow w \subseteq y)$
120	119	anbi2d	$⊢ z = y \to ((A \in w \land w \subseteq z) \leftrightarrow (A \in w \land w \subseteq y))$
121	120	rexbidv	$⊢ z = y \to (\exists w \in x (A \in w \land w \subseteq z) \leftrightarrow \exists w \in x (A \in w \land w \subseteq y))$
122	118 121	imbi12d	$⊢ z = y \to ((A \in z \to \exists w \in x (A \in w \land w \subseteq z)) \leftrightarrow (A \in y \to \exists w \in x (A \in w \land w \subseteq y)))$
123	122	rspccva	$⊢ (\forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z)) \land y \in J) \to (A \in y \to \exists w \in x (A \in w \land w \subseteq y))$
124	117 123	sylan	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (A \in y \to \exists w \in x (A \in w \land w \subseteq y))$
125		eleq2w	$⊢ a = w \to (A \in a \leftrightarrow A \in w)$
126	125	rexrab	$⊢ \exists w \in \{a \in x \| A \in a\} w \subseteq y \leftrightarrow \exists w \in x (A \in w \land w \subseteq y)$
127	43	rexeqdv	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to (\exists w \in ran g w \subseteq y \leftrightarrow \exists w \in \{a \in x \| A \in a\} w \subseteq y)$
128		fofn	$⊢ g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\} \to g Fn ℕ$
129	128	ad2antll	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to g Fn ℕ$
130		sseq1	$⊢ w = g (k) \to (w \subseteq y \leftrightarrow g (k) \subseteq y)$
131	130	rexrn	$⊢ g Fn ℕ \to (\exists w \in ran g w \subseteq y \leftrightarrow \exists k \in ℕ g (k) \subseteq y)$
132	129 131	syl	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to (\exists w \in ran g w \subseteq y \leftrightarrow \exists k \in ℕ g (k) \subseteq y)$
133	127 132	bitr3d	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to (\exists w \in \{a \in x \| A \in a\} w \subseteq y \leftrightarrow \exists k \in ℕ g (k) \subseteq y)$
134	133	adantr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (\exists w \in \{a \in x \| A \in a\} w \subseteq y \leftrightarrow \exists k \in ℕ g (k) \subseteq y)$
135		elfz1end	$⊢ k \in ℕ \leftrightarrow k \in (1 \dots k)$
136		fz1ssnn	$⊢ (1 \dots k) \subseteq ℕ$
137	53	adantr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to dom g = ℕ$
138	136 137	sseqtrrid	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (1 \dots k) \subseteq dom g$
139		funfvima2	$⊢ (Fun g \land (1 \dots k) \subseteq dom g) \to (k \in (1 \dots k) \to g (k) \in g [(1 \dots k)])$
140	67 138 139	syl2an2r	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (k \in (1 \dots k) \to g (k) \in g [(1 \dots k)])$
141	140	imp	$⊢ ((((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \land k \in (1 \dots k)) \to g (k) \in g [(1 \dots k)]$
142	135 141	sylan2b	$⊢ ((((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \land k \in ℕ) \to g (k) \in g [(1 \dots k)]$
143		intss1	$⊢ g (k) \in g [(1 \dots k)] \to ⋂ g [(1 \dots k)] \subseteq g (k)$
144		sstr2	$⊢ ⋂ g [(1 \dots k)] \subseteq g (k) \to (g (k) \subseteq y \to ⋂ g [(1 \dots k)] \subseteq y)$
145	142 143 144	3syl	$⊢ ((((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \land k \in ℕ) \to (g (k) \subseteq y \to ⋂ g [(1 \dots k)] \subseteq y)$
146	145	reximdva	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (\exists k \in ℕ g (k) \subseteq y \to \exists k \in ℕ ⋂ g [(1 \dots k)] \subseteq y)$
147	134 146	sylbid	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (\exists w \in \{a \in x \| A \in a\} w \subseteq y \to \exists k \in ℕ ⋂ g [(1 \dots k)] \subseteq y)$
148	126 147	syl5bir	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (\exists w \in x (A \in w \land w \subseteq y) \to \exists k \in ℕ ⋂ g [(1 \dots k)] \subseteq y)$
149	124 148	syld	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (A \in y \to \exists k \in ℕ ⋂ g [(1 \dots k)] \subseteq y)$
150	98	sseq1d	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land k \in ℕ) \to ((n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y \leftrightarrow ⋂ g [(1 \dots k)] \subseteq y)$
151	150	rexbidva	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to (\exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y \leftrightarrow \exists k \in ℕ ⋂ g [(1 \dots k)] \subseteq y)$
152	151	adantr	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (\exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y \leftrightarrow \exists k \in ℕ ⋂ g [(1 \dots k)] \subseteq y)$
153	149 152	sylibrd	$⊢ (((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \land y \in J) \to (A \in y \to \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y)$
154	153	ralrimiva	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to \forall y \in J (A \in y \to \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y)$
155		nnex	$⊢ ℕ \in V$
156	155	mptex	$⊢ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \in V$
157		feq1	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (f : ℕ ⟶ J \leftrightarrow (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) : ℕ ⟶ J)$
158		fveq1	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to f (k) = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)$
159	158	eleq2d	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (A \in f (k) \leftrightarrow A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k))$
160		fveq1	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to f (k + 1) = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1)$
161	160 158	sseq12d	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (f (k + 1) \subseteq f (k) \leftrightarrow (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k))$
162	159 161	anbi12d	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to ((A \in f (k) \land f (k + 1) \subseteq f (k)) \leftrightarrow (A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \land (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)))$
163	162	ralbidv	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (\forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \leftrightarrow \forall k \in ℕ (A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \land (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)))$
164	158	sseq1d	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (f (k) \subseteq y \leftrightarrow (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y)$
165	164	rexbidv	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (\exists k \in ℕ f (k) \subseteq y \leftrightarrow \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y)$
166	165	imbi2d	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to ((A \in y \to \exists k \in ℕ f (k) \subseteq y) \leftrightarrow (A \in y \to \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y))$
167	166	ralbidv	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to (\forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y) \leftrightarrow \forall y \in J (A \in y \to \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y))$
168	157 163 167	3anbi123d	$⊢ f = (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) \to ((f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y)) \leftrightarrow ((n \in ℕ ⟼ ⋂ g [(1 \dots n)]) : ℕ ⟶ J \land \forall k \in ℕ (A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \land (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y)))$
169	156 168	spcev	$⊢ ((n \in ℕ ⟼ ⋂ g [(1 \dots n)]) : ℕ ⟶ J \land \forall k \in ℕ (A \in (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \land (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k + 1) \subseteq (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ (n \in ℕ ⟼ ⋂ g [(1 \dots n)]) (k) \subseteq y)) \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y))$
170	75 116 154 169	syl3anc	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land ((x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))) \land g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\})) \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y))$
171	170	expr	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z)))) \to (g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\} \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y)))$
172	171	adantrrl	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to (g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\} \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y)))$
173	172	exlimdv	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to (\exists g g : ℕ \underset{onto}{⟶} \{a \in x \| A \in a\} \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y)))$
174	39 173	mpd	$⊢ ((J \in 1^{st} 𝜔 \land A \in X) \land (x \in 𝒫 J \land (x ≼ ω \land \forall z \in J (A \in z \to \exists w \in x (A \in w \land w \subseteq z))))) \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y))$
175	2 174	rexlimddv	$⊢ (J \in 1^{st} 𝜔 \land A \in X) \to \exists f (f : ℕ ⟶ J \land \forall k \in ℕ (A \in f (k) \land f (k + 1) \subseteq f (k)) \land \forall y \in J (A \in y \to \exists k \in ℕ f (k) \subseteq y))$

Metamath Proof Explorer

Theorem 1stcfb

Proof