tgrest

Description: A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015) (Proof shortened by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	tgrest	$⊢ (B \in V \land A \in W) \to topGen (B ↾_{𝑡} A) = topGen (B) ↾_{𝑡} A$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ B ↾_{𝑡} A \in V$
2		eltg3	$⊢ B ↾_{𝑡} A \in V \to (x \in topGen (B ↾_{𝑡} A) \leftrightarrow \exists y (y \subseteq B ↾_{𝑡} A \land x = ⋃ y))$
3	1 2	ax-mp	$⊢ x \in topGen (B ↾_{𝑡} A) \leftrightarrow \exists y (y \subseteq B ↾_{𝑡} A \land x = ⋃ y)$
4		simpll	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to B \in V$
5		funmpt	$⊢ Fun (x \in B ⟼ x \cap A)$
6	5	a1i	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to Fun (x \in B ⟼ x \cap A)$
7		restval	$⊢ (B \in V \land A \in W) \to B ↾_{𝑡} A = ran (x \in B ⟼ x \cap A)$
8	7	sseq2d	$⊢ (B \in V \land A \in W) \to (y \subseteq B ↾_{𝑡} A \leftrightarrow y \subseteq ran (x \in B ⟼ x \cap A))$
9	8	biimpa	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to y \subseteq ran (x \in B ⟼ x \cap A)$
10		vex	$⊢ x \in V$
11	10	inex1	$⊢ x \cap A \in V$
12	11	rgenw	$⊢ \forall x \in B x \cap A \in V$
13		eqid	$⊢ (x \in B ⟼ x \cap A) = (x \in B ⟼ x \cap A)$
14	13	fnmpt	$⊢ \forall x \in B x \cap A \in V \to (x \in B ⟼ x \cap A) Fn B$
15		fnima	$⊢ (x \in B ⟼ x \cap A) Fn B \to (x \in B ⟼ x \cap A) [B] = ran (x \in B ⟼ x \cap A)$
16	12 14 15	mp2b	$⊢ (x \in B ⟼ x \cap A) [B] = ran (x \in B ⟼ x \cap A)$
17	9 16	sseqtrrdi	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to y \subseteq (x \in B ⟼ x \cap A) [B]$
18		ssimaexg	$⊢ (B \in V \land Fun (x \in B ⟼ x \cap A) \land y \subseteq (x \in B ⟼ x \cap A) [B]) \to \exists z (z \subseteq B \land y = (x \in B ⟼ x \cap A) [z])$
19	4 6 17 18	syl3anc	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to \exists z (z \subseteq B \land y = (x \in B ⟼ x \cap A) [z])$
20		df-ima	$⊢ (x \in B ⟼ x \cap A) [z] = ran ({(x \in B ⟼ x \cap A) ↾}_{z})$
21		resmpt	$⊢ z \subseteq B \to {(x \in B ⟼ x \cap A) ↾}_{z} = (x \in z ⟼ x \cap A)$
22	21	adantl	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to {(x \in B ⟼ x \cap A) ↾}_{z} = (x \in z ⟼ x \cap A)$
23	22	rneqd	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ran ({(x \in B ⟼ x \cap A) ↾}_{z}) = ran (x \in z ⟼ x \cap A)$
24	20 23	eqtrid	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to (x \in B ⟼ x \cap A) [z] = ran (x \in z ⟼ x \cap A)$
25	24	unieqd	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃ (x \in B ⟼ x \cap A) [z] = ⋃ ran (x \in z ⟼ x \cap A)$
26	11	dfiun3	$⊢ ⋃_{x \in z} (x \cap A) = ⋃ ran (x \in z ⟼ x \cap A)$
27	25 26	eqtr4di	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃ (x \in B ⟼ x \cap A) [z] = ⋃_{x \in z} (x \cap A)$
28		iunin1	$⊢ ⋃_{x \in z} (x \cap A) = ⋃_{x \in z} x \cap A$
29	27 28	eqtrdi	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃ (x \in B ⟼ x \cap A) [z] = ⋃_{x \in z} x \cap A$
30		fvex	$⊢ topGen (B) \in V$
31		simpr	$⊢ (B \in V \land A \in W) \to A \in W$
32		uniiun	$⊢ ⋃ z = ⋃_{x \in z} x$
33		eltg3i	$⊢ (B \in V \land z \subseteq B) \to ⋃ z \in topGen (B)$
34	32 33	eqeltrrid	$⊢ (B \in V \land z \subseteq B) \to ⋃_{x \in z} x \in topGen (B)$
35	34	adantlr	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃_{x \in z} x \in topGen (B)$
36		elrestr	$⊢ (topGen (B) \in V \land A \in W \land ⋃_{x \in z} x \in topGen (B)) \to ⋃_{x \in z} x \cap A \in (topGen (B) ↾_{𝑡} A)$
37	30 31 35 36	mp3an2ani	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃_{x \in z} x \cap A \in (topGen (B) ↾_{𝑡} A)$
38	29 37	eqeltrd	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃ (x \in B ⟼ x \cap A) [z] \in (topGen (B) ↾_{𝑡} A)$
39		unieq	$⊢ y = (x \in B ⟼ x \cap A) [z] \to ⋃ y = ⋃ (x \in B ⟼ x \cap A) [z]$
40	39	eleq1d	$⊢ y = (x \in B ⟼ x \cap A) [z] \to (⋃ y \in (topGen (B) ↾_{𝑡} A) \leftrightarrow ⋃ (x \in B ⟼ x \cap A) [z] \in (topGen (B) ↾_{𝑡} A))$
41	38 40	syl5ibrcom	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to (y = (x \in B ⟼ x \cap A) [z] \to ⋃ y \in (topGen (B) ↾_{𝑡} A))$
42	41	expimpd	$⊢ (B \in V \land A \in W) \to ((z \subseteq B \land y = (x \in B ⟼ x \cap A) [z]) \to ⋃ y \in (topGen (B) ↾_{𝑡} A))$
43	42	exlimdv	$⊢ (B \in V \land A \in W) \to (\exists z (z \subseteq B \land y = (x \in B ⟼ x \cap A) [z]) \to ⋃ y \in (topGen (B) ↾_{𝑡} A))$
44	43	adantr	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to (\exists z (z \subseteq B \land y = (x \in B ⟼ x \cap A) [z]) \to ⋃ y \in (topGen (B) ↾_{𝑡} A))$
45	19 44	mpd	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to ⋃ y \in (topGen (B) ↾_{𝑡} A)$
46		eleq1	$⊢ x = ⋃ y \to (x \in (topGen (B) ↾_{𝑡} A) \leftrightarrow ⋃ y \in (topGen (B) ↾_{𝑡} A))$
47	45 46	syl5ibrcom	$⊢ ((B \in V \land A \in W) \land y \subseteq B ↾_{𝑡} A) \to (x = ⋃ y \to x \in (topGen (B) ↾_{𝑡} A))$
48	47	expimpd	$⊢ (B \in V \land A \in W) \to ((y \subseteq B ↾_{𝑡} A \land x = ⋃ y) \to x \in (topGen (B) ↾_{𝑡} A))$
49	48	exlimdv	$⊢ (B \in V \land A \in W) \to (\exists y (y \subseteq B ↾_{𝑡} A \land x = ⋃ y) \to x \in (topGen (B) ↾_{𝑡} A))$
50	3 49	biimtrid	$⊢ (B \in V \land A \in W) \to (x \in topGen (B ↾_{𝑡} A) \to x \in (topGen (B) ↾_{𝑡} A))$
51	50	ssrdv	$⊢ (B \in V \land A \in W) \to topGen (B ↾_{𝑡} A) \subseteq topGen (B) ↾_{𝑡} A$
52		restval	$⊢ (topGen (B) \in V \land A \in W) \to topGen (B) ↾_{𝑡} A = ran (w \in topGen (B) ⟼ w \cap A)$
53	30 31 52	sylancr	$⊢ (B \in V \land A \in W) \to topGen (B) ↾_{𝑡} A = ran (w \in topGen (B) ⟼ w \cap A)$
54		eltg3	$⊢ B \in V \to (w \in topGen (B) \leftrightarrow \exists z (z \subseteq B \land w = ⋃ z))$
55	54	adantr	$⊢ (B \in V \land A \in W) \to (w \in topGen (B) \leftrightarrow \exists z (z \subseteq B \land w = ⋃ z))$
56	32	ineq1i	$⊢ ⋃ z \cap A = ⋃_{x \in z} x \cap A$
57	56 28	eqtr4i	$⊢ ⋃ z \cap A = ⋃_{x \in z} (x \cap A)$
58		simplll	$⊢ (((B \in V \land A \in W) \land z \subseteq B) \land x \in z) \to B \in V$
59		simpllr	$⊢ (((B \in V \land A \in W) \land z \subseteq B) \land x \in z) \to A \in W$
60		simpr	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to z \subseteq B$
61	60	sselda	$⊢ (((B \in V \land A \in W) \land z \subseteq B) \land x \in z) \to x \in B$
62		elrestr	$⊢ (B \in V \land A \in W \land x \in B) \to x \cap A \in (B ↾_{𝑡} A)$
63	58 59 61 62	syl3anc	$⊢ (((B \in V \land A \in W) \land z \subseteq B) \land x \in z) \to x \cap A \in (B ↾_{𝑡} A)$
64	63	fmpttd	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to (x \in z ⟼ x \cap A) : z ⟶ B ↾_{𝑡} A$
65	64	frnd	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ran (x \in z ⟼ x \cap A) \subseteq B ↾_{𝑡} A$
66		eltg3i	$⊢ (B ↾_{𝑡} A \in V \land ran (x \in z ⟼ x \cap A) \subseteq B ↾_{𝑡} A) \to ⋃ ran (x \in z ⟼ x \cap A) \in topGen (B ↾_{𝑡} A)$
67	1 65 66	sylancr	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃ ran (x \in z ⟼ x \cap A) \in topGen (B ↾_{𝑡} A)$
68	26 67	eqeltrid	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃_{x \in z} (x \cap A) \in topGen (B ↾_{𝑡} A)$
69	57 68	eqeltrid	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to ⋃ z \cap A \in topGen (B ↾_{𝑡} A)$
70		ineq1	$⊢ w = ⋃ z \to w \cap A = ⋃ z \cap A$
71	70	eleq1d	$⊢ w = ⋃ z \to (w \cap A \in topGen (B ↾_{𝑡} A) \leftrightarrow ⋃ z \cap A \in topGen (B ↾_{𝑡} A))$
72	69 71	syl5ibrcom	$⊢ ((B \in V \land A \in W) \land z \subseteq B) \to (w = ⋃ z \to w \cap A \in topGen (B ↾_{𝑡} A))$
73	72	expimpd	$⊢ (B \in V \land A \in W) \to ((z \subseteq B \land w = ⋃ z) \to w \cap A \in topGen (B ↾_{𝑡} A))$
74	73	exlimdv	$⊢ (B \in V \land A \in W) \to (\exists z (z \subseteq B \land w = ⋃ z) \to w \cap A \in topGen (B ↾_{𝑡} A))$
75	55 74	sylbid	$⊢ (B \in V \land A \in W) \to (w \in topGen (B) \to w \cap A \in topGen (B ↾_{𝑡} A))$
76	75	imp	$⊢ ((B \in V \land A \in W) \land w \in topGen (B)) \to w \cap A \in topGen (B ↾_{𝑡} A)$
77	76	fmpttd	$⊢ (B \in V \land A \in W) \to (w \in topGen (B) ⟼ w \cap A) : topGen (B) ⟶ topGen (B ↾_{𝑡} A)$
78	77	frnd	$⊢ (B \in V \land A \in W) \to ran (w \in topGen (B) ⟼ w \cap A) \subseteq topGen (B ↾_{𝑡} A)$
79	53 78	eqsstrd	$⊢ (B \in V \land A \in W) \to topGen (B) ↾_{𝑡} A \subseteq topGen (B ↾_{𝑡} A)$
80	51 79	eqssd	$⊢ (B \in V \land A \in W) \to topGen (B ↾_{𝑡} A) = topGen (B) ↾_{𝑡} A$

Metamath Proof Explorer

Theorem tgrest

Proof