1stcrest

Description: A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	1stcrest	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to J ↾_{𝑡} A \in 1^{st} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		1stctop	$⊢ J \in 1^{st} 𝜔 \to J \in Top$
2		resttop	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$
3	1 2	sylan	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to J ↾_{𝑡} A \in Top$
4		eqid	$⊢ ⋃ J = ⋃ J$
5	4	restuni2	$⊢ (J \in Top \land A \in V) \to A \cap ⋃ J = ⋃ (J ↾_{𝑡} A)$
6	1 5	sylan	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to A \cap ⋃ J = ⋃ (J ↾_{𝑡} A)$
7	6	eleq2d	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to (x \in (A \cap ⋃ J) \leftrightarrow x \in ⋃ (J ↾_{𝑡} A))$
8	7	biimpar	$⊢ ((J \in 1^{st} 𝜔 \land A \in V) \land x \in ⋃ (J ↾_{𝑡} A)) \to x \in (A \cap ⋃ J)$
9		simpl	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to J \in 1^{st} 𝜔$
10		elinel2	$⊢ x \in (A \cap ⋃ J) \to x \in ⋃ J$
11	4	1stcclb	$⊢ (J \in 1^{st} 𝜔 \land x \in ⋃ J) \to \exists t \in 𝒫 J (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a)))$
12	9 10 11	syl2an	$⊢ ((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \to \exists t \in 𝒫 J (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a)))$
13		simplll	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to J \in 1^{st} 𝜔$
14		elpwi	$⊢ t \in 𝒫 J \to t \subseteq J$
15	14	ad2antrl	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to t \subseteq J$
16		ssrest	$⊢ (J \in 1^{st} 𝜔 \land t \subseteq J) \to t ↾_{𝑡} A \subseteq J ↾_{𝑡} A$
17	13 15 16	syl2anc	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to t ↾_{𝑡} A \subseteq J ↾_{𝑡} A$
18		ovex	$⊢ J ↾_{𝑡} A \in V$
19	18	elpw2	$⊢ t ↾_{𝑡} A \in 𝒫 (J ↾_{𝑡} A) \leftrightarrow t ↾_{𝑡} A \subseteq J ↾_{𝑡} A$
20	17 19	sylibr	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to t ↾_{𝑡} A \in 𝒫 (J ↾_{𝑡} A)$
21		vex	$⊢ t \in V$
22		simpllr	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to A \in V$
23		restval	$⊢ (t \in V \land A \in V) \to t ↾_{𝑡} A = ran (v \in t ⟼ v \cap A)$
24	21 22 23	sylancr	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to t ↾_{𝑡} A = ran (v \in t ⟼ v \cap A)$
25		simprrl	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to t ≼ ω$
26		1stcrestlem	$⊢ t ≼ ω \to ran (v \in t ⟼ v \cap A) ≼ ω$
27	25 26	syl	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to ran (v \in t ⟼ v \cap A) ≼ ω$
28	24 27	eqbrtrd	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to (t ↾_{𝑡} A) ≼ ω$
29	1	ad3antrrr	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to J \in Top$
30		elrest	$⊢ (J \in Top \land A \in V) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists a \in J z = a \cap A)$
31	29 22 30	syl2anc	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists a \in J z = a \cap A)$
32		r19.29	$⊢ (\forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \land \exists a \in J z = a \cap A) \to \exists a \in J ((x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \land z = a \cap A)$
33		simprr	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to x \in A$
34	33	a1d	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (x \in y \to x \in A)$
35	34	ancld	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (x \in y \to (x \in y \land x \in A))$
36		elin	$⊢ x \in (y \cap A) \leftrightarrow (x \in y \land x \in A)$
37	35 36	imbitrrdi	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (x \in y \to x \in (y \cap A))$
38		ssrin	$⊢ y \subseteq a \to y \cap A \subseteq a \cap A$
39	37 38	anim12d1	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to ((x \in y \land y \subseteq a) \to (x \in (y \cap A) \land y \cap A \subseteq a \cap A))$
40	39	reximdv	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (\exists y \in t (x \in y \land y \subseteq a) \to \exists y \in t (x \in (y \cap A) \land y \cap A \subseteq a \cap A))$
41		vex	$⊢ y \in V$
42	41	inex1	$⊢ y \cap A \in V$
43	42	a1i	$⊢ (((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \land y \in t) \to y \cap A \in V$
44		simp-4r	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to A \in V$
45		elrest	$⊢ (t \in V \land A \in V) \to (w \in (t ↾_{𝑡} A) \leftrightarrow \exists y \in t w = y \cap A)$
46	21 44 45	sylancr	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (w \in (t ↾_{𝑡} A) \leftrightarrow \exists y \in t w = y \cap A)$
47		eleq2	$⊢ w = y \cap A \to (x \in w \leftrightarrow x \in (y \cap A))$
48		sseq1	$⊢ w = y \cap A \to (w \subseteq a \cap A \leftrightarrow y \cap A \subseteq a \cap A)$
49	47 48	anbi12d	$⊢ w = y \cap A \to ((x \in w \land w \subseteq a \cap A) \leftrightarrow (x \in (y \cap A) \land y \cap A \subseteq a \cap A))$
50	49	adantl	$⊢ (((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \land w = y \cap A) \to ((x \in w \land w \subseteq a \cap A) \leftrightarrow (x \in (y \cap A) \land y \cap A \subseteq a \cap A))$
51	43 46 50	rexxfr2d	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (\exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A) \leftrightarrow \exists y \in t (x \in (y \cap A) \land y \cap A \subseteq a \cap A))$
52	40 51	sylibrd	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land (a \in J \land x \in A)) \to (\exists y \in t (x \in y \land y \subseteq a) \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A))$
53	52	expr	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land a \in J) \to (x \in A \to (\exists y \in t (x \in y \land y \subseteq a) \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A)))$
54	53	com23	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land a \in J) \to (\exists y \in t (x \in y \land y \subseteq a) \to (x \in A \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A)))$
55	54	imim2d	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land a \in J) \to ((x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \to (x \in a \to (x \in A \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A))))$
56	55	imp4b	$⊢ (((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land a \in J) \land (x \in a \to \exists y \in t (x \in y \land y \subseteq a))) \to ((x \in a \land x \in A) \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A))$
57		eleq2	$⊢ z = a \cap A \to (x \in z \leftrightarrow x \in (a \cap A))$
58		elin	$⊢ x \in (a \cap A) \leftrightarrow (x \in a \land x \in A)$
59	57 58	bitrdi	$⊢ z = a \cap A \to (x \in z \leftrightarrow (x \in a \land x \in A))$
60		sseq2	$⊢ z = a \cap A \to (w \subseteq z \leftrightarrow w \subseteq a \cap A)$
61	60	anbi2d	$⊢ z = a \cap A \to ((x \in w \land w \subseteq z) \leftrightarrow (x \in w \land w \subseteq a \cap A))$
62	61	rexbidv	$⊢ z = a \cap A \to (\exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z) \leftrightarrow \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A))$
63	59 62	imbi12d	$⊢ z = a \cap A \to ((x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)) \leftrightarrow ((x \in a \land x \in A) \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq a \cap A)))$
64	56 63	syl5ibrcom	$⊢ (((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land a \in J) \land (x \in a \to \exists y \in t (x \in y \land y \subseteq a))) \to (z = a \cap A \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
65	64	expimpd	$⊢ ((((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \land a \in J) \to (((x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \land z = a \cap A) \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
66	65	rexlimdva	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \to (\exists a \in J ((x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \land z = a \cap A) \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
67	32 66	syl5	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \to ((\forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \land \exists a \in J z = a \cap A) \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
68	67	expd	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land t \in 𝒫 J) \to (\forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a)) \to (\exists a \in J z = a \cap A \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z))))$
69	68	impr	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a)))) \to (\exists a \in J z = a \cap A \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
70	69	adantrrl	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to (\exists a \in J z = a \cap A \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
71	31 70	sylbid	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to (z \in (J ↾_{𝑡} A) \to (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
72	71	ralrimiv	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z))$
73		breq1	$⊢ y = t ↾_{𝑡} A \to (y ≼ ω \leftrightarrow (t ↾_{𝑡} A) ≼ ω)$
74		rexeq	$⊢ y = t ↾_{𝑡} A \to (\exists w \in y (x \in w \land w \subseteq z) \leftrightarrow \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z))$
75	74	imbi2d	$⊢ y = t ↾_{𝑡} A \to ((x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
76	75	ralbidv	$⊢ y = t ↾_{𝑡} A \to (\forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))$
77	73 76	anbi12d	$⊢ y = t ↾_{𝑡} A \to ((y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow ((t ↾_{𝑡} A) ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z))))$
78	77	rspcev	$⊢ (t ↾_{𝑡} A \in 𝒫 (J ↾_{𝑡} A) \land ((t ↾_{𝑡} A) ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in (t ↾_{𝑡} A) (x \in w \land w \subseteq z)))) \to \exists y \in 𝒫 (J ↾_{𝑡} A) (y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
79	20 28 72 78	syl12anc	$⊢ (((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \land (t \in 𝒫 J \land (t ≼ ω \land \forall a \in J (x \in a \to \exists y \in t (x \in y \land y \subseteq a))))) \to \exists y \in 𝒫 (J ↾_{𝑡} A) (y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
80	12 79	rexlimddv	$⊢ ((J \in 1^{st} 𝜔 \land A \in V) \land x \in (A \cap ⋃ J)) \to \exists y \in 𝒫 (J ↾_{𝑡} A) (y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
81	8 80	syldan	$⊢ ((J \in 1^{st} 𝜔 \land A \in V) \land x \in ⋃ (J ↾_{𝑡} A)) \to \exists y \in 𝒫 (J ↾_{𝑡} A) (y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
82	81	ralrimiva	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to \forall x \in ⋃ (J ↾_{𝑡} A) \exists y \in 𝒫 (J ↾_{𝑡} A) (y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
83		eqid	$⊢ ⋃ (J ↾_{𝑡} A) = ⋃ (J ↾_{𝑡} A)$
84	83	is1stc2	$⊢ J ↾_{𝑡} A \in 1^{st} 𝜔 \leftrightarrow (J ↾_{𝑡} A \in Top \land \forall x \in ⋃ (J ↾_{𝑡} A) \exists y \in 𝒫 (J ↾_{𝑡} A) (y ≼ ω \land \forall z \in (J ↾_{𝑡} A) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))$
85	3 82 84	sylanbrc	$⊢ (J \in 1^{st} 𝜔 \land A \in V) \to J ↾_{𝑡} A \in 1^{st} 𝜔$

Metamath Proof Explorer

Theorem 1stcrest

Proof