tgcmp

Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub , which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	tgcmp	$⊢ (B \in TopBases \land X = ⋃ B) \to (topGen (B) \in Comp \leftrightarrow \forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ topGen (B) = ⋃ topGen (B)$
2	1	iscmp	$⊢ topGen (B) \in Comp \leftrightarrow (topGen (B) \in Top \land \forall y \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ topGen (B) = ⋃ z))$
3	2	simprbi	$⊢ topGen (B) \in Comp \to \forall y \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ topGen (B) = ⋃ z)$
4		unitg	$⊢ B \in TopBases \to ⋃ topGen (B) = ⋃ B$
5		eqtr3	$⊢ (⋃ topGen (B) = ⋃ B \land X = ⋃ B) \to ⋃ topGen (B) = X$
6	4 5	sylan	$⊢ (B \in TopBases \land X = ⋃ B) \to ⋃ topGen (B) = X$
7	6	eqeq1d	$⊢ (B \in TopBases \land X = ⋃ B) \to (⋃ topGen (B) = ⋃ y \leftrightarrow X = ⋃ y)$
8	6	eqeq1d	$⊢ (B \in TopBases \land X = ⋃ B) \to (⋃ topGen (B) = ⋃ z \leftrightarrow X = ⋃ z)$
9	8	rexbidv	$⊢ (B \in TopBases \land X = ⋃ B) \to (\exists z \in (𝒫 y \cap Fin) ⋃ topGen (B) = ⋃ z \leftrightarrow \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
10	7 9	imbi12d	$⊢ (B \in TopBases \land X = ⋃ B) \to ((⋃ topGen (B) = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ topGen (B) = ⋃ z) \leftrightarrow (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
11	10	ralbidv	$⊢ (B \in TopBases \land X = ⋃ B) \to (\forall y \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ topGen (B) = ⋃ z) \leftrightarrow \forall y \in 𝒫 topGen (B) (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
12		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
13	12	adantr	$⊢ (B \in TopBases \land X = ⋃ B) \to B \subseteq topGen (B)$
14	13	sspwd	$⊢ (B \in TopBases \land X = ⋃ B) \to 𝒫 B \subseteq 𝒫 topGen (B)$
15		ssralv	$⊢ 𝒫 B \subseteq 𝒫 topGen (B) \to (\forall y \in 𝒫 topGen (B) (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
16	14 15	syl	$⊢ (B \in TopBases \land X = ⋃ B) \to (\forall y \in 𝒫 topGen (B) (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
17	11 16	sylbid	$⊢ (B \in TopBases \land X = ⋃ B) \to (\forall y \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ topGen (B) = ⋃ z) \to \forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
18	3 17	syl5	$⊢ (B \in TopBases \land X = ⋃ B) \to (topGen (B) \in Comp \to \forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
19		elpwi	$⊢ u \in 𝒫 topGen (B) \to u \subseteq topGen (B)$
20		simprr	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to X = ⋃ u$
21		simprl	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to u \subseteq topGen (B)$
22	21	sselda	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land t \in u) \to t \in topGen (B)$
23	22	adantrr	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (t \in u \land y \in t)) \to t \in topGen (B)$
24		simprr	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (t \in u \land y \in t)) \to y \in t$
25		tg2	$⊢ (t \in topGen (B) \land y \in t) \to \exists w \in B (y \in w \land w \subseteq t)$
26	23 24 25	syl2anc	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (t \in u \land y \in t)) \to \exists w \in B (y \in w \land w \subseteq t)$
27	26	expr	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land t \in u) \to (y \in t \to \exists w \in B (y \in w \land w \subseteq t))$
28	27	reximdva	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (\exists t \in u y \in t \to \exists t \in u \exists w \in B (y \in w \land w \subseteq t))$
29		eluni2	$⊢ y \in ⋃ u \leftrightarrow \exists t \in u y \in t$
30		elunirab	$⊢ y \in ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \leftrightarrow \exists w \in B (y \in w \land \exists t \in u w \subseteq t)$
31		r19.42v	$⊢ \exists t \in u (y \in w \land w \subseteq t) \leftrightarrow (y \in w \land \exists t \in u w \subseteq t)$
32	31	rexbii	$⊢ \exists w \in B \exists t \in u (y \in w \land w \subseteq t) \leftrightarrow \exists w \in B (y \in w \land \exists t \in u w \subseteq t)$
33		rexcom	$⊢ \exists w \in B \exists t \in u (y \in w \land w \subseteq t) \leftrightarrow \exists t \in u \exists w \in B (y \in w \land w \subseteq t)$
34	30 32 33	3bitr2i	$⊢ y \in ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \leftrightarrow \exists t \in u \exists w \in B (y \in w \land w \subseteq t)$
35	28 29 34	3imtr4g	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (y \in ⋃ u \to y \in ⋃ \{w \in B \| \exists t \in u w \subseteq t\})$
36	35	ssrdv	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to ⋃ u \subseteq ⋃ \{w \in B \| \exists t \in u w \subseteq t\}$
37	20 36	eqsstrd	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to X \subseteq ⋃ \{w \in B \| \exists t \in u w \subseteq t\}$
38		ssrab2	$⊢ \{w \in B \| \exists t \in u w \subseteq t\} \subseteq B$
39	38	unissi	$⊢ ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \subseteq ⋃ B$
40		simplr	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to X = ⋃ B$
41	39 40	sseqtrrid	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \subseteq X$
42	37 41	eqssd	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to X = ⋃ \{w \in B \| \exists t \in u w \subseteq t\}$
43		elpw2g	$⊢ B \in TopBases \to (\{w \in B \| \exists t \in u w \subseteq t\} \in 𝒫 B \leftrightarrow \{w \in B \| \exists t \in u w \subseteq t\} \subseteq B)$
44	43	ad2antrr	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (\{w \in B \| \exists t \in u w \subseteq t\} \in 𝒫 B \leftrightarrow \{w \in B \| \exists t \in u w \subseteq t\} \subseteq B)$
45	38 44	mpbiri	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to \{w \in B \| \exists t \in u w \subseteq t\} \in 𝒫 B$
46		unieq	$⊢ y = \{w \in B \| \exists t \in u w \subseteq t\} \to ⋃ y = ⋃ \{w \in B \| \exists t \in u w \subseteq t\}$
47	46	eqeq2d	$⊢ y = \{w \in B \| \exists t \in u w \subseteq t\} \to (X = ⋃ y \leftrightarrow X = ⋃ \{w \in B \| \exists t \in u w \subseteq t\})$
48		pweq	$⊢ y = \{w \in B \| \exists t \in u w \subseteq t\} \to 𝒫 y = 𝒫 \{w \in B \| \exists t \in u w \subseteq t\}$
49	48	ineq1d	$⊢ y = \{w \in B \| \exists t \in u w \subseteq t\} \to 𝒫 y \cap Fin = 𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin$
50	49	rexeqdv	$⊢ y = \{w \in B \| \exists t \in u w \subseteq t\} \to (\exists z \in (𝒫 y \cap Fin) X = ⋃ z \leftrightarrow \exists z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) X = ⋃ z)$
51	47 50	imbi12d	$⊢ y = \{w \in B \| \exists t \in u w \subseteq t\} \to ((X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \leftrightarrow (X = ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \to \exists z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) X = ⋃ z))$
52	51	rspcv	$⊢ \{w \in B \| \exists t \in u w \subseteq t\} \in 𝒫 B \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to (X = ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \to \exists z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) X = ⋃ z))$
53	45 52	syl	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to (X = ⋃ \{w \in B \| \exists t \in u w \subseteq t\} \to \exists z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) X = ⋃ z))$
54	42 53	mpid	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \exists z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) X = ⋃ z)$
55		elfpw	$⊢ z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \leftrightarrow (z \subseteq \{w \in B \| \exists t \in u w \subseteq t\} \land z \in Fin)$
56	55	simprbi	$⊢ z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \to z \in Fin$
57	56	ad2antrl	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \to z \in Fin$
58	55	simplbi	$⊢ z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \to z \subseteq \{w \in B \| \exists t \in u w \subseteq t\}$
59	58	ad2antrl	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \to z \subseteq \{w \in B \| \exists t \in u w \subseteq t\}$
60		ssrab	$⊢ z \subseteq \{w \in B \| \exists t \in u w \subseteq t\} \leftrightarrow (z \subseteq B \land \forall w \in z \exists t \in u w \subseteq t)$
61	60	simprbi	$⊢ z \subseteq \{w \in B \| \exists t \in u w \subseteq t\} \to \forall w \in z \exists t \in u w \subseteq t$
62	59 61	syl	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \to \forall w \in z \exists t \in u w \subseteq t$
63		sseq2	$⊢ t = f (w) \to (w \subseteq t \leftrightarrow w \subseteq f (w))$
64	63	ac6sfi	$⊢ (z \in Fin \land \forall w \in z \exists t \in u w \subseteq t) \to \exists f (f : z ⟶ u \land \forall w \in z w \subseteq f (w))$
65	57 62 64	syl2anc	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \to \exists f (f : z ⟶ u \land \forall w \in z w \subseteq f (w))$
66		frn	$⊢ f : z ⟶ u \to ran f \subseteq u$
67	66	ad2antrl	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ran f \subseteq u$
68		ffn	$⊢ f : z ⟶ u \to f Fn z$
69		dffn4	$⊢ f Fn z \leftrightarrow f : z \underset{onto}{⟶} ran f$
70	68 69	sylib	$⊢ f : z ⟶ u \to f : z \underset{onto}{⟶} ran f$
71	70	adantr	$⊢ (f : z ⟶ u \land \forall w \in z w \subseteq f (w)) \to f : z \underset{onto}{⟶} ran f$
72		fofi	$⊢ (z \in Fin \land f : z \underset{onto}{⟶} ran f) \to ran f \in Fin$
73	57 71 72	syl2an	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ran f \in Fin$
74		elfpw	$⊢ ran f \in (𝒫 u \cap Fin) \leftrightarrow (ran f \subseteq u \land ran f \in Fin)$
75	67 73 74	sylanbrc	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ran f \in (𝒫 u \cap Fin)$
76		simplrr	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to X = ⋃ z$
77		uniiun	$⊢ ⋃ z = ⋃_{w \in z} w$
78		ss2iun	$⊢ \forall w \in z w \subseteq f (w) \to ⋃_{w \in z} w \subseteq ⋃_{w \in z} f (w)$
79	77 78	eqsstrid	$⊢ \forall w \in z w \subseteq f (w) \to ⋃ z \subseteq ⋃_{w \in z} f (w)$
80	79	ad2antll	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ⋃ z \subseteq ⋃_{w \in z} f (w)$
81		fniunfv	$⊢ f Fn z \to ⋃_{w \in z} f (w) = ⋃ ran f$
82	68 81	syl	$⊢ f : z ⟶ u \to ⋃_{w \in z} f (w) = ⋃ ran f$
83	82	ad2antrl	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ⋃_{w \in z} f (w) = ⋃ ran f$
84	80 83	sseqtrd	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ⋃ z \subseteq ⋃ ran f$
85	76 84	eqsstrd	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to X \subseteq ⋃ ran f$
86	67	unissd	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ⋃ ran f \subseteq ⋃ u$
87	20	ad2antrr	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to X = ⋃ u$
88	86 87	sseqtrrd	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to ⋃ ran f \subseteq X$
89	85 88	eqssd	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to X = ⋃ ran f$
90		unieq	$⊢ v = ran f \to ⋃ v = ⋃ ran f$
91	90	rspceeqv	$⊢ (ran f \in (𝒫 u \cap Fin) \land X = ⋃ ran f) \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v$
92	75 89 91	syl2anc	$⊢ ((((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \land (f : z ⟶ u \land \forall w \in z w \subseteq f (w))) \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v$
93	65 92	exlimddv	$⊢ (((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \land (z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) \land X = ⋃ z)) \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v$
94	93	rexlimdvaa	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (\exists z \in (𝒫 \{w \in B \| \exists t \in u w \subseteq t\} \cap Fin) X = ⋃ z \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v)$
95	54 94	syld	$⊢ ((B \in TopBases \land X = ⋃ B) \land (u \subseteq topGen (B) \land X = ⋃ u)) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v)$
96	95	expr	$⊢ ((B \in TopBases \land X = ⋃ B) \land u \subseteq topGen (B)) \to (X = ⋃ u \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
97	96	com23	$⊢ ((B \in TopBases \land X = ⋃ B) \land u \subseteq topGen (B)) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to (X = ⋃ u \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
98	19 97	sylan2	$⊢ ((B \in TopBases \land X = ⋃ B) \land u \in 𝒫 topGen (B)) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to (X = ⋃ u \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
99	98	ralrimdva	$⊢ (B \in TopBases \land X = ⋃ B) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \forall u \in 𝒫 topGen (B) (X = ⋃ u \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
100		tgcl	$⊢ B \in TopBases \to topGen (B) \in Top$
101	100	adantr	$⊢ (B \in TopBases \land X = ⋃ B) \to topGen (B) \in Top$
102	1	iscmp	$⊢ topGen (B) \in Comp \leftrightarrow (topGen (B) \in Top \land \forall u \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ u \to \exists v \in (𝒫 u \cap Fin) ⋃ topGen (B) = ⋃ v))$
103	102	baib	$⊢ topGen (B) \in Top \to (topGen (B) \in Comp \leftrightarrow \forall u \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ u \to \exists v \in (𝒫 u \cap Fin) ⋃ topGen (B) = ⋃ v))$
104	101 103	syl	$⊢ (B \in TopBases \land X = ⋃ B) \to (topGen (B) \in Comp \leftrightarrow \forall u \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ u \to \exists v \in (𝒫 u \cap Fin) ⋃ topGen (B) = ⋃ v))$
105	6	eqeq1d	$⊢ (B \in TopBases \land X = ⋃ B) \to (⋃ topGen (B) = ⋃ u \leftrightarrow X = ⋃ u)$
106	6	eqeq1d	$⊢ (B \in TopBases \land X = ⋃ B) \to (⋃ topGen (B) = ⋃ v \leftrightarrow X = ⋃ v)$
107	106	rexbidv	$⊢ (B \in TopBases \land X = ⋃ B) \to (\exists v \in (𝒫 u \cap Fin) ⋃ topGen (B) = ⋃ v \leftrightarrow \exists v \in (𝒫 u \cap Fin) X = ⋃ v)$
108	105 107	imbi12d	$⊢ (B \in TopBases \land X = ⋃ B) \to ((⋃ topGen (B) = ⋃ u \to \exists v \in (𝒫 u \cap Fin) ⋃ topGen (B) = ⋃ v) \leftrightarrow (X = ⋃ u \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
109	108	ralbidv	$⊢ (B \in TopBases \land X = ⋃ B) \to (\forall u \in 𝒫 topGen (B) (⋃ topGen (B) = ⋃ u \to \exists v \in (𝒫 u \cap Fin) ⋃ topGen (B) = ⋃ v) \leftrightarrow \forall u \in 𝒫 topGen (B) (X = ⋃ u \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
110	104 109	bitrd	$⊢ (B \in TopBases \land X = ⋃ B) \to (topGen (B) \in Comp \leftrightarrow \forall u \in 𝒫 topGen (B) (X = ⋃ u \to \exists v \in (𝒫 u \cap Fin) X = ⋃ v))$
111	99 110	sylibrd	$⊢ (B \in TopBases \land X = ⋃ B) \to (\forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to topGen (B) \in Comp)$
112	18 111	impbid	$⊢ (B \in TopBases \land X = ⋃ B) \to (topGen (B) \in Comp \leftrightarrow \forall y \in 𝒫 B (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$

Metamath Proof Explorer

Theorem tgcmp

Proof