lly1stc

Description: First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	lly1stc	$⊢ Locally1^{st} 𝜔=1^{st} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		llytop	$⊢ j \in Locally1^{st} 𝜔\toj \in Top$
2		simprr	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\toj ↾_{𝑡} u \in 1^{st} 𝜔)))$
3		simprl	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\tox \in u)))$
4	1	ad3antrrr	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\toj \in Top)))$
5		elssuni	$⊢ u \in j \to u \subseteq ⋃ j$
6	5	ad2antlr	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\tou \subseteq ⋃ j)))$
7		eqid	$⊢ ⋃ j = ⋃ j$
8	7	restuni	$⊢ (j \in Top \land u \subseteq ⋃ j) \to u = ⋃ (j ↾_{𝑡} u)$
9	4 6 8	syl2anc	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\tou = ⋃ (j ↾_{𝑡} u))))$
10	3 9	eleqtrd	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\tox \in ⋃ (j ↾_{𝑡} u))))$
11		eqid	$⊢ ⋃ (j ↾_{𝑡} u) = ⋃ (j ↾_{𝑡} u)$
12	11	1stcclb	$⊢ (j ↾_{𝑡} u \in 1^{st} 𝜔 \land x \in ⋃ (j ↾_{𝑡} u)) \to \exists t \in 𝒫 (j ↾_{𝑡} u) (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v)))$
13	2 10 12	syl2anc	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\to\exists t \in 𝒫 (j ↾_{𝑡} u) (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))))$
14		elpwi	$⊢ t \in 𝒫 (j ↾_{𝑡} u) \to t \subseteq j ↾_{𝑡} u$
15	14	adantl	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\tot \subseteq j ↾_{𝑡} u))))$
16	15	sselda	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\ton \in (j ↾_{𝑡} u))))))$
17	4	adantr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\toj \in Top))))$
18		simpllr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\tou \in j))))$
19		restopn2	$⊢ (j \in Top \land u \in j) \to (n \in (j ↾_{𝑡} u) \leftrightarrow (n \in j \land n \subseteq u))$
20	17 18 19	syl2anc	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\to(n \in (j ↾_{𝑡} u) \leftrightarrow (n \in j \land n \subseteq u))))))$
21	20	simplbda	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in (j ↾_{𝑡} u)\ton \subseteq u)))))$
22	16 21	syldan	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\ton \subseteq u)))))$
23		df-ss	$⊢ n \subseteq u \leftrightarrow n \cap u = n$
24	22 23	sylib	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\ton \cap u = n)))))$
25	20	simprbda	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in (j ↾_{𝑡} u)\ton \in j)))))$
26	16 25	syldan	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\ton \in j)))))$
27	24 26	eqeltrd	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\ton \cap u \in j)))))$
28		ineq1	$⊢ a = n \to a \cap u = n \cap u$
29	28	cbvmptv	$⊢ (a \in t ⟼ a \cap u) = (n \in t ⟼ n \cap u)$
30	27 29	fmptd	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\to(a \in t ⟼ a \cap u) : t ⟶ j))))$
31	30	frnd	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\toran (a \in t ⟼ a \cap u) \subseteq j))))$
32	31	adantrr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\toran (a \in t ⟼ a \cap u) \subseteq j))))$
33		vex	$⊢ j \in V$
34	33	elpw2	$⊢ ran (a \in t ⟼ a \cap u) \in 𝒫 j \leftrightarrow ran (a \in t ⟼ a \cap u) \subseteq j$
35	32 34	sylibr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\toran (a \in t ⟼ a \cap u) \in 𝒫 j))))$
36		simprrl	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\tot ≼ ω))))$
37		1stcrestlem	$⊢ t ≼ ω \to ran (a \in t ⟼ a \cap u) ≼ ω$
38	36 37	syl	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\toran (a \in t ⟼ a \cap u) ≼ ω))))$
39		simprr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\tox \in z)))))$
40	3	ad2antrr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\tox \in u)))))$
41	39 40	elind	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\tox \in (z \cap u))))))$
42		eleq2	$⊢ v = z \cap u \to (x \in v \leftrightarrow x \in (z \cap u))$
43		sseq2	$⊢ v = z \cap u \to (n \subseteq v \leftrightarrow n \subseteq z \cap u)$
44	43	anbi2d	$⊢ v = z \cap u \to ((x \in n \land n \subseteq v) \leftrightarrow (x \in n \land n \subseteq z \cap u))$
45	44	rexbidv	$⊢ v = z \cap u \to (\exists n \in t (x \in n \land n \subseteq v) \leftrightarrow \exists n \in t (x \in n \land n \subseteq z \cap u))$
46	42 45	imbi12d	$⊢ v = z \cap u \to ((x \in v \to \exists n \in t (x \in n \land n \subseteq v)) \leftrightarrow (x \in (z \cap u) \to \exists n \in t (x \in n \land n \subseteq z \cap u)))$
47		simprrr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\to\forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))))$
48	47	adantr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\to\forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v)))))))$
49	4	ad2antrr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\toj \in Top)))))$
50		simpllr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\tou \in j))))$
51	50	adantr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\tou \in j)))))$
52		simprl	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\toz \in j)))))$
53		elrestr	$⊢ (j \in Top \land u \in j \land z \in j) \to z \cap u \in (j ↾_{𝑡} u)$
54	49 51 52 53	syl3anc	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\toz \cap u \in (j ↾_{𝑡} u))))))$
55	46 48 54	rspcdva	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\to(x \in (z \cap u) \to \exists n \in t (x \in n \land n \subseteq z \cap u)))))))$
56	41 55	mpd	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\to\exists n \in t (x \in n \land n \subseteq z \cap u))))))$
57	3	ad2antrr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\tox \in u)))))$
58		elin	$⊢ x \in (n \cap u) \leftrightarrow (x \in n \land x \in u)$
59	58	simplbi2com	$⊢ x \in u \to (x \in n \to x \in (n \cap u))$
60	57 59	syl	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\to(x \in n \to x \in (n \cap u)))))))$
61	22	biantrud	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\to(n \subseteq z \leftrightarrow (n \subseteq z \land n \subseteq u)))))))$
62		ssin	$⊢ (n \subseteq z \land n \subseteq u) \leftrightarrow n \subseteq z \cap u$
63	61 62	bitrdi	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\to(n \subseteq z \leftrightarrow n \subseteq z \cap u))))))$
64		ssinss1	$⊢ n \subseteq z \to n \cap u \subseteq z$
65	63 64	syl6bir	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\to(n \subseteq z \cap u \to n \cap u \subseteq z))))))$
66	60 65	anim12d	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\landn \in t\to((x \in n \land n \subseteq z \cap u) \to (x \in (n \cap u) \land n \cap u \subseteq z)))))))$
67	66	reximdva	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\to(\exists n \in t (x \in n \land n \subseteq z \cap u) \to \exists n \in t (x \in (n \cap u) \land n \cap u \subseteq z))))))$
68		vex	$⊢ n \in V$
69	68	inex1	$⊢ n \cap u \in V$
70	69	rgenw	$⊢ \forall n \in t n \cap u \in V$
71		eleq2	$⊢ w = n \cap u \to (x \in w \leftrightarrow x \in (n \cap u))$
72		sseq1	$⊢ w = n \cap u \to (w \subseteq z \leftrightarrow n \cap u \subseteq z)$
73	71 72	anbi12d	$⊢ w = n \cap u \to ((x \in w \land w \subseteq z) \leftrightarrow (x \in (n \cap u) \land n \cap u \subseteq z))$
74	29 73	rexrnmptw	$⊢ \forall n \in t n \cap u \in V \to (\exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z) \leftrightarrow \exists n \in t (x \in (n \cap u) \land n \cap u \subseteq z))$
75	70 74	ax-mp	$⊢ \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z) \leftrightarrow \exists n \in t (x \in (n \cap u) \land n \cap u \subseteq z)$
76	67 75	syl6ibr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\landt \in 𝒫 (j ↾_{𝑡} u)\to(\exists n \in t (x \in n \land n \subseteq z \cap u) \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z))))))$
77	76	adantrr	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\to(\exists n \in t (x \in n \land n \subseteq z \cap u) \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z))))))$
78	77	adantr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\to(\exists n \in t (x \in n \land n \subseteq z \cap u) \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z)))))))$
79	56 78	mpd	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\land(z \in j \land x \in z)\to\exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z))))))$
80	79	expr	$⊢ (((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\landz \in j\to(x \in z \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z)))))))$
81	80	ralrimiva	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\to\forall z \in j (x \in z \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z))))))$
82		breq1	$⊢ y = ran (a \in t ⟼ a \cap u) \to (y ≼ ω \leftrightarrow ran (a \in t ⟼ a \cap u) ≼ ω)$
83		rexeq	$⊢ y = ran (a \in t ⟼ a \cap u) \to (\exists w \in y (x \in w \land w \subseteq z) \leftrightarrow \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z))$
84	83	imbi2d	$⊢ y = ran (a \in t ⟼ a \cap u) \to ((x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow (x \in z \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z)))$
85	84	ralbidv	$⊢ y = ran (a \in t ⟼ a \cap u) \to (\forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow \forall z \in j (x \in z \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z)))$
86	82 85	anbi12d	$⊢ y = ran (a \in t ⟼ a \cap u) \to ((y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow (ran (a \in t ⟼ a \cap u) ≼ ω \land \forall z \in j (x \in z \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z))))$
87	86	rspcev	$⊢ (ran (a \in t ⟼ a \cap u) \in 𝒫 j \land (ran (a \in t ⟼ a \cap u) ≼ ω \land \forall z \in j (x \in z \to \exists w \in ran (a \in t ⟼ a \cap u) (x \in w \land w \subseteq z)))) \to \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
88	35 38 81 87	syl12anc	$⊢ ((((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\land(t \in 𝒫 (j ↾_{𝑡} u) \land (t ≼ ω \land \forall v \in (j ↾_{𝑡} u) (x \in v \to \exists n \in t (x \in n \land n \subseteq v))))\to\exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))))))$
89	13 88	rexlimddv	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\to\exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))))$
90	89	3adantr1	$⊢ (((j \in Locally1^{st} 𝜔\landx \in ⋃ j\landu \in j\land(u \subseteq ⋃ j \land x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔)\to\exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))))$
91		simpl	$⊢ (j \in Locally1^{st} 𝜔\landx \in ⋃ j\toj \in Locally1^{st} 𝜔)$
92	1	adantr	$⊢ (j \in Locally1^{st} 𝜔\landx \in ⋃ j\toj \in Top)$
93	7	topopn	$⊢ j \in Top \to ⋃ j \in j$
94	92 93	syl	$⊢ (j \in Locally1^{st} 𝜔\landx \in ⋃ j\to⋃ j \in j)$
95		simpr	$⊢ (j \in Locally1^{st} 𝜔\landx \in ⋃ j\tox \in ⋃ j)$
96		llyi	$⊢ (j \in Locally1^{st} 𝜔\land⋃ j \in j\landx \in ⋃ j\to\exists u \in j (u \subseteq ⋃ j \land x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔))$
97	91 94 95 96	syl3anc	$⊢ (j \in Locally1^{st} 𝜔\landx \in ⋃ j\to\exists u \in j (u \subseteq ⋃ j \land x \in u \land j ↾_{𝑡} u \in 1^{st} 𝜔))$
98	90 97	r19.29a	$⊢ (j \in Locally1^{st} 𝜔\landx \in ⋃ j\to\exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))$
99	98	ralrimiva	$⊢ j \in Locally1^{st} 𝜔\to\forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
100	7	is1stc2	$⊢ j \in 1^{st} 𝜔 \leftrightarrow (j \in Top \land \forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))$
101	1 99 100	sylanbrc	$⊢ j \in Locally1^{st} 𝜔\toj \in 1^{st} 𝜔$
102	101	ssriv	$⊢ Locally1^{st} 𝜔\subseteq1^{st} 𝜔$
103		1stcrest	$⊢ (j \in 1^{st} 𝜔 \land x \in j) \to j ↾_{𝑡} x \in 1^{st} 𝜔$
104	103	adantl	$⊢ (⊤ \land (j \in 1^{st} 𝜔 \land x \in j)) \to j ↾_{𝑡} x \in 1^{st} 𝜔$
105		1stctop	$⊢ j \in 1^{st} 𝜔 \to j \in Top$
106	105	ssriv	$⊢ 1^{st} 𝜔 \subseteq Top$
107	106	a1i	$⊢ ⊤ \to 1^{st} 𝜔 \subseteq Top$
108	104 107	restlly	$⊢ ⊤ \to 1^{st} 𝜔 \subseteq Locally1^{st} 𝜔$
109	108	mptru	$⊢ 1^{st} 𝜔 \subseteq Locally1^{st} 𝜔$
110	102 109	eqssi	$⊢ Locally1^{st} 𝜔=1^{st} 𝜔$

Metamath Proof Explorer

Theorem lly1stc

Proof