alexsubb

Description: Biconditional form of the Alexander Subbase Theorem alexsub . (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	alexsubb	$⊢ (X \in UFL \land X = ⋃ B) \to (topGen (fi (B)) \in Comp \leftrightarrow \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ topGen (fi (B)) = ⋃ topGen (fi (B))$
2	1	iscmp	$⊢ topGen (fi (B)) \in Comp \leftrightarrow (topGen (fi (B)) \in Top \land \forall x \in 𝒫 topGen (fi (B)) (⋃ topGen (fi (B)) = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ topGen (fi (B)) = ⋃ y))$
3	2	simprbi	$⊢ topGen (fi (B)) \in Comp \to \forall x \in 𝒫 topGen (fi (B)) (⋃ topGen (fi (B)) = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ topGen (fi (B)) = ⋃ y)$
4		simpr	$⊢ (X \in UFL \land X = ⋃ B) \to X = ⋃ B$
5		elex	$⊢ X \in UFL \to X \in V$
6	5	adantr	$⊢ (X \in UFL \land X = ⋃ B) \to X \in V$
7	4 6	eqeltrrd	$⊢ (X \in UFL \land X = ⋃ B) \to ⋃ B \in V$
8		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
9	7 8	sylibr	$⊢ (X \in UFL \land X = ⋃ B) \to B \in V$
10		fiuni	$⊢ B \in V \to ⋃ B = ⋃ fi (B)$
11	9 10	syl	$⊢ (X \in UFL \land X = ⋃ B) \to ⋃ B = ⋃ fi (B)$
12		fibas	$⊢ fi (B) \in TopBases$
13		unitg	$⊢ fi (B) \in TopBases \to ⋃ topGen (fi (B)) = ⋃ fi (B)$
14	12 13	mp1i	$⊢ (X \in UFL \land X = ⋃ B) \to ⋃ topGen (fi (B)) = ⋃ fi (B)$
15	11 4 14	3eqtr4d	$⊢ (X \in UFL \land X = ⋃ B) \to X = ⋃ topGen (fi (B))$
16	15	eqeq1d	$⊢ (X \in UFL \land X = ⋃ B) \to (X = ⋃ x \leftrightarrow ⋃ topGen (fi (B)) = ⋃ x)$
17	15	eqeq1d	$⊢ (X \in UFL \land X = ⋃ B) \to (X = ⋃ y \leftrightarrow ⋃ topGen (fi (B)) = ⋃ y)$
18	17	rexbidv	$⊢ (X \in UFL \land X = ⋃ B) \to (\exists y \in (𝒫 x \cap Fin) X = ⋃ y \leftrightarrow \exists y \in (𝒫 x \cap Fin) ⋃ topGen (fi (B)) = ⋃ y)$
19	16 18	imbi12d	$⊢ (X \in UFL \land X = ⋃ B) \to ((X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \leftrightarrow (⋃ topGen (fi (B)) = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ topGen (fi (B)) = ⋃ y))$
20	19	ralbidv	$⊢ (X \in UFL \land X = ⋃ B) \to (\forall x \in 𝒫 topGen (fi (B)) (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \leftrightarrow \forall x \in 𝒫 topGen (fi (B)) (⋃ topGen (fi (B)) = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ topGen (fi (B)) = ⋃ y))$
21		ssfii	$⊢ B \in V \to B \subseteq fi (B)$
22	9 21	syl	$⊢ (X \in UFL \land X = ⋃ B) \to B \subseteq fi (B)$
23		bastg	$⊢ fi (B) \in TopBases \to fi (B) \subseteq topGen (fi (B))$
24	12 23	ax-mp	$⊢ fi (B) \subseteq topGen (fi (B))$
25	22 24	sstrdi	$⊢ (X \in UFL \land X = ⋃ B) \to B \subseteq topGen (fi (B))$
26	25	sspwd	$⊢ (X \in UFL \land X = ⋃ B) \to 𝒫 B \subseteq 𝒫 topGen (fi (B))$
27		ssralv	$⊢ 𝒫 B \subseteq 𝒫 topGen (fi (B)) \to (\forall x \in 𝒫 topGen (fi (B)) (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \to \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y))$
28	26 27	syl	$⊢ (X \in UFL \land X = ⋃ B) \to (\forall x \in 𝒫 topGen (fi (B)) (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \to \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y))$
29	20 28	sylbird	$⊢ (X \in UFL \land X = ⋃ B) \to (\forall x \in 𝒫 topGen (fi (B)) (⋃ topGen (fi (B)) = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ topGen (fi (B)) = ⋃ y) \to \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y))$
30	3 29	syl5	$⊢ (X \in UFL \land X = ⋃ B) \to (topGen (fi (B)) \in Comp \to \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y))$
31		simpll	$⊢ ((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \to X \in UFL$
32		simplr	$⊢ ((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \to X = ⋃ B$
33		eqidd	$⊢ ((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \to topGen (fi (B)) = topGen (fi (B))$
34		velpw	$⊢ z \in 𝒫 B \leftrightarrow z \subseteq B$
35		unieq	$⊢ x = z \to ⋃ x = ⋃ z$
36	35	eqeq2d	$⊢ x = z \to (X = ⋃ x \leftrightarrow X = ⋃ z)$
37		pweq	$⊢ x = z \to 𝒫 x = 𝒫 z$
38	37	ineq1d	$⊢ x = z \to 𝒫 x \cap Fin = 𝒫 z \cap Fin$
39	38	rexeqdv	$⊢ x = z \to (\exists y \in (𝒫 x \cap Fin) X = ⋃ y \leftrightarrow \exists y \in (𝒫 z \cap Fin) X = ⋃ y)$
40	36 39	imbi12d	$⊢ x = z \to ((X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \leftrightarrow (X = ⋃ z \to \exists y \in (𝒫 z \cap Fin) X = ⋃ y))$
41	40	rspccv	$⊢ \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \to (z \in 𝒫 B \to (X = ⋃ z \to \exists y \in (𝒫 z \cap Fin) X = ⋃ y))$
42	41	adantl	$⊢ ((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \to (z \in 𝒫 B \to (X = ⋃ z \to \exists y \in (𝒫 z \cap Fin) X = ⋃ y))$
43	34 42	syl5bir	$⊢ ((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \to (z \subseteq B \to (X = ⋃ z \to \exists y \in (𝒫 z \cap Fin) X = ⋃ y))$
44	43	imp32	$⊢ (((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \land (z \subseteq B \land X = ⋃ z)) \to \exists y \in (𝒫 z \cap Fin) X = ⋃ y$
45		unieq	$⊢ y = w \to ⋃ y = ⋃ w$
46	45	eqeq2d	$⊢ y = w \to (X = ⋃ y \leftrightarrow X = ⋃ w)$
47	46	cbvrexvw	$⊢ \exists y \in (𝒫 z \cap Fin) X = ⋃ y \leftrightarrow \exists w \in (𝒫 z \cap Fin) X = ⋃ w$
48	44 47	sylib	$⊢ (((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \land (z \subseteq B \land X = ⋃ z)) \to \exists w \in (𝒫 z \cap Fin) X = ⋃ w$
49	31 32 33 48	alexsub	$⊢ ((X \in UFL \land X = ⋃ B) \land \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y)) \to topGen (fi (B)) \in Comp$
50	49	ex	$⊢ (X \in UFL \land X = ⋃ B) \to (\forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \to topGen (fi (B)) \in Comp)$
51	30 50	impbid	$⊢ (X \in UFL \land X = ⋃ B) \to (topGen (fi (B)) \in Comp \leftrightarrow \forall x \in 𝒫 B (X = ⋃ x \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y))$

Metamath Proof Explorer

Theorem alexsubb

Proof