alexsubALT

Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010) (Revised by Mario Carneiro, 11-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	alexsubALT.1	$⊢ X = ⋃ J$
	Assertion	alexsubALT	$⊢ J \in Comp \leftrightarrow \exists x (J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$

Proof

Step	Hyp	Ref	Expression
1		alexsubALT.1	$⊢ X = ⋃ J$
2	1	alexsubALTlem1	$⊢ J \in Comp \to \exists x (J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
3	1	alexsubALTlem4	$⊢ J = topGen (fi (x)) \to (\forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to \forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
4		velpw	$⊢ c \in 𝒫 J \leftrightarrow c \subseteq J$
5		eleq2	$⊢ X = ⋃ c \to (t \in X \leftrightarrow t \in ⋃ c)$
6	5	3ad2ant3	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in X \leftrightarrow t \in ⋃ c)$
7		eluni	$⊢ t \in ⋃ c \leftrightarrow \exists w (t \in w \land w \in c)$
8		ssel	$⊢ c \subseteq J \to (w \in c \to w \in J)$
9		eleq2	$⊢ J = topGen (fi (x)) \to (w \in J \leftrightarrow w \in topGen (fi (x)))$
10		tg2	$⊢ (w \in topGen (fi (x)) \land t \in w) \to \exists y \in fi (x) (t \in y \land y \subseteq w)$
11	10	ex	$⊢ w \in topGen (fi (x)) \to (t \in w \to \exists y \in fi (x) (t \in y \land y \subseteq w))$
12	9 11	biimtrdi	$⊢ J = topGen (fi (x)) \to (w \in J \to (t \in w \to \exists y \in fi (x) (t \in y \land y \subseteq w)))$
13	8 12	sylan9r	$⊢ (J = topGen (fi (x)) \land c \subseteq J) \to (w \in c \to (t \in w \to \exists y \in fi (x) (t \in y \land y \subseteq w)))$
14	13	3impia	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land w \in c) \to (t \in w \to \exists y \in fi (x) (t \in y \land y \subseteq w))$
15		sseq2	$⊢ z = w \to (y \subseteq z \leftrightarrow y \subseteq w)$
16	15	rspcev	$⊢ (w \in c \land y \subseteq w) \to \exists z \in c y \subseteq z$
17	16	ex	$⊢ w \in c \to (y \subseteq w \to \exists z \in c y \subseteq z)$
18	17	3ad2ant3	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land w \in c) \to (y \subseteq w \to \exists z \in c y \subseteq z)$
19	18	anim2d	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land w \in c) \to ((t \in y \land y \subseteq w) \to (t \in y \land \exists z \in c y \subseteq z))$
20	19	reximdv	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land w \in c) \to (\exists y \in fi (x) (t \in y \land y \subseteq w) \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
21	14 20	syld	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land w \in c) \to (t \in w \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
22	21	3expia	$⊢ (J = topGen (fi (x)) \land c \subseteq J) \to (w \in c \to (t \in w \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z)))$
23	22	com23	$⊢ (J = topGen (fi (x)) \land c \subseteq J) \to (t \in w \to (w \in c \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z)))$
24	23	impd	$⊢ (J = topGen (fi (x)) \land c \subseteq J) \to ((t \in w \land w \in c) \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
25	24	exlimdv	$⊢ (J = topGen (fi (x)) \land c \subseteq J) \to (\exists w (t \in w \land w \in c) \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
26	7 25	biimtrid	$⊢ (J = topGen (fi (x)) \land c \subseteq J) \to (t \in ⋃ c \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
27	26	3adant3	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in ⋃ c \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
28	6 27	sylbid	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in X \to \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
29		ssel	$⊢ y \subseteq z \to (t \in y \to t \in z)$
30		elunii	$⊢ (t \in z \land z \in c) \to t \in ⋃ c$
31	30	expcom	$⊢ z \in c \to (t \in z \to t \in ⋃ c)$
32	6	biimprd	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in ⋃ c \to t \in X)$
33	31 32	sylan9r	$⊢ ((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land z \in c) \to (t \in z \to t \in X)$
34	29 33	syl9r	$⊢ ((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land z \in c) \to (y \subseteq z \to (t \in y \to t \in X))$
35	34	rexlimdva	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (\exists z \in c y \subseteq z \to (t \in y \to t \in X))$
36	35	com23	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in y \to (\exists z \in c y \subseteq z \to t \in X))$
37	36	impd	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to ((t \in y \land \exists z \in c y \subseteq z) \to t \in X)$
38	37	rexlimdvw	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (\exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z) \to t \in X)$
39	28 38	impbid	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in X \leftrightarrow \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z))$
40		elunirab	$⊢ t \in ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \leftrightarrow \exists y \in fi (x) (t \in y \land \exists z \in c y \subseteq z)$
41	39 40	bitr4di	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (t \in X \leftrightarrow t \in ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\})$
42	41	eqrdv	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to X = ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\}$
43		ssrab2	$⊢ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \subseteq fi (x)$
44		fvex	$⊢ fi (x) \in V$
45	44	elpw2	$⊢ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \in 𝒫 fi (x) \leftrightarrow \{y \in fi (x) \| \exists z \in c y \subseteq z\} \subseteq fi (x)$
46	43 45	mpbir	$⊢ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \in 𝒫 fi (x)$
47		unieq	$⊢ a = \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to ⋃ a = ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\}$
48	47	eqeq2d	$⊢ a = \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (X = ⋃ a \leftrightarrow X = ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\})$
49		pweq	$⊢ a = \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to 𝒫 a = 𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\}$
50	49	ineq1d	$⊢ a = \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to 𝒫 a \cap Fin = 𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin$
51	50	rexeqdv	$⊢ a = \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (\exists b \in (𝒫 a \cap Fin) X = ⋃ b \leftrightarrow \exists b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) X = ⋃ b)$
52	48 51	imbi12d	$⊢ a = \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to ((X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \leftrightarrow (X = ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \exists b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) X = ⋃ b))$
53	52	rspcv	$⊢ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \in 𝒫 fi (x) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to (X = ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \exists b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) X = ⋃ b))$
54	46 53	ax-mp	$⊢ \forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to (X = ⋃ \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \exists b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) X = ⋃ b)$
55	42 54	syl5com	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to \exists b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) X = ⋃ b)$
56		elfpw	$⊢ b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) \leftrightarrow (b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \land b \in Fin)$
57		ssel	$⊢ b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (t \in b \to t \in \{y \in fi (x) \| \exists z \in c y \subseteq z\})$
58		sseq1	$⊢ y = t \to (y \subseteq z \leftrightarrow t \subseteq z)$
59	58	rexbidv	$⊢ y = t \to (\exists z \in c y \subseteq z \leftrightarrow \exists z \in c t \subseteq z)$
60	59	elrab	$⊢ t \in \{y \in fi (x) \| \exists z \in c y \subseteq z\} \leftrightarrow (t \in fi (x) \land \exists z \in c t \subseteq z)$
61	60	simprbi	$⊢ t \in \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \exists z \in c t \subseteq z$
62	57 61	syl6	$⊢ b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (t \in b \to \exists z \in c t \subseteq z)$
63	62	ralrimiv	$⊢ b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \forall t \in b \exists z \in c t \subseteq z$
64		sseq2	$⊢ z = f (t) \to (t \subseteq z \leftrightarrow t \subseteq f (t))$
65	64	ac6sfi	$⊢ (b \in Fin \land \forall t \in b \exists z \in c t \subseteq z) \to \exists f (f : b ⟶ c \land \forall t \in b t \subseteq f (t))$
66	65	ex	$⊢ b \in Fin \to (\forall t \in b \exists z \in c t \subseteq z \to \exists f (f : b ⟶ c \land \forall t \in b t \subseteq f (t)))$
67	63 66	syl5	$⊢ b \in Fin \to (b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \exists f (f : b ⟶ c \land \forall t \in b t \subseteq f (t)))$
68	67	adantl	$⊢ ((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \to (b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to \exists f (f : b ⟶ c \land \forall t \in b t \subseteq f (t)))$
69		simprll	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to f : b ⟶ c$
70		frn	$⊢ f : b ⟶ c \to ran f \subseteq c$
71	69 70	syl	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ran f \subseteq c$
72		simplr	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to b \in Fin$
73		ffn	$⊢ f : b ⟶ c \to f Fn b$
74		dffn4	$⊢ f Fn b \leftrightarrow f : b \underset{onto}{⟶} ran f$
75	73 74	sylib	$⊢ f : b ⟶ c \to f : b \underset{onto}{⟶} ran f$
76	75	adantr	$⊢ (f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \to f : b \underset{onto}{⟶} ran f$
77	76	ad2antrl	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to f : b \underset{onto}{⟶} ran f$
78		fodomfi	$⊢ (b \in Fin \land f : b \underset{onto}{⟶} ran f) \to ran f ≼ b$
79	72 77 78	syl2anc	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ran f ≼ b$
80		domfi	$⊢ (b \in Fin \land ran f ≼ b) \to ran f \in Fin$
81	72 79 80	syl2anc	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ran f \in Fin$
82	71 81	jca	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to (ran f \subseteq c \land ran f \in Fin)$
83		elin	$⊢ ran f \in (𝒫 c \cap Fin) \leftrightarrow (ran f \in 𝒫 c \land ran f \in Fin)$
84		vex	$⊢ c \in V$
85	84	elpw2	$⊢ ran f \in 𝒫 c \leftrightarrow ran f \subseteq c$
86	85	anbi1i	$⊢ (ran f \in 𝒫 c \land ran f \in Fin) \leftrightarrow (ran f \subseteq c \land ran f \in Fin)$
87	83 86	bitr2i	$⊢ (ran f \subseteq c \land ran f \in Fin) \leftrightarrow ran f \in (𝒫 c \cap Fin)$
88	82 87	sylib	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ran f \in (𝒫 c \cap Fin)$
89		simprr	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to X = ⋃ b$
90		uniiun	$⊢ ⋃ b = ⋃_{t \in b} t$
91		simprlr	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to \forall t \in b t \subseteq f (t)$
92		ss2iun	$⊢ \forall t \in b t \subseteq f (t) \to ⋃_{t \in b} t \subseteq ⋃_{t \in b} f (t)$
93	91 92	syl	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ⋃_{t \in b} t \subseteq ⋃_{t \in b} f (t)$
94	90 93	eqsstrid	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ⋃ b \subseteq ⋃_{t \in b} f (t)$
95		fniunfv	$⊢ f Fn b \to ⋃_{t \in b} f (t) = ⋃ ran f$
96	69 73 95	3syl	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ⋃_{t \in b} f (t) = ⋃ ran f$
97	94 96	sseqtrd	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ⋃ b \subseteq ⋃ ran f$
98	89 97	eqsstrd	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to X \subseteq ⋃ ran f$
99		simpll2	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to c \subseteq J$
100	71 99	sstrd	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ran f \subseteq J$
101		uniss	$⊢ ran f \subseteq J \to ⋃ ran f \subseteq ⋃ J$
102	101 1	sseqtrrdi	$⊢ ran f \subseteq J \to ⋃ ran f \subseteq X$
103	100 102	syl	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to ⋃ ran f \subseteq X$
104	98 103	eqssd	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to X = ⋃ ran f$
105		unieq	$⊢ d = ran f \to ⋃ d = ⋃ ran f$
106	105	eqeq2d	$⊢ d = ran f \to (X = ⋃ d \leftrightarrow X = ⋃ ran f)$
107	106	rspcev	$⊢ (ran f \in (𝒫 c \cap Fin) \land X = ⋃ ran f) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d$
108	88 104 107	syl2anc	$⊢ (((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \land ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \land X = ⋃ b)) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d$
109	108	exp32	$⊢ ((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \to ((f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
110	109	exlimdv	$⊢ ((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \to (\exists f (f : b ⟶ c \land \forall t \in b t \subseteq f (t)) \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
111	68 110	syld	$⊢ ((J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \land b \in Fin) \to (b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
112	111	ex	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (b \in Fin \to (b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
113	112	com23	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \to (b \in Fin \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
114	113	impd	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to ((b \subseteq \{y \in fi (x) \| \exists z \in c y \subseteq z\} \land b \in Fin) \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
115	56 114	biimtrid	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) \to (X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
116	115	rexlimdv	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (\exists b \in (𝒫 \{y \in fi (x) \| \exists z \in c y \subseteq z\} \cap Fin) X = ⋃ b \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
117	55 116	syld	$⊢ (J = topGen (fi (x)) \land c \subseteq J \land X = ⋃ c) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
118	117	3exp	$⊢ J = topGen (fi (x)) \to (c \subseteq J \to (X = ⋃ c \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
119	118	com34	$⊢ J = topGen (fi (x)) \to (c \subseteq J \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
120	119	com23	$⊢ J = topGen (fi (x)) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to (c \subseteq J \to (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
121	4 120	syl7bi	$⊢ J = topGen (fi (x)) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to (c \in 𝒫 J \to (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
122	121	ralrimdv	$⊢ J = topGen (fi (x)) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
123		fibas	$⊢ fi (x) \in TopBases$
124		tgcl	$⊢ fi (x) \in TopBases \to topGen (fi (x)) \in Top$
125	123 124	ax-mp	$⊢ topGen (fi (x)) \in Top$
126		eleq1	$⊢ J = topGen (fi (x)) \to (J \in Top \leftrightarrow topGen (fi (x)) \in Top)$
127	125 126	mpbiri	$⊢ J = topGen (fi (x)) \to J \in Top$
128	122 127	jctild	$⊢ J = topGen (fi (x)) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to (J \in Top \land \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)))$
129	1	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
130	128 129	imbitrrdi	$⊢ J = topGen (fi (x)) \to (\forall a \in 𝒫 fi (x) (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \to J \in Comp)$
131	3 130	syld	$⊢ J = topGen (fi (x)) \to (\forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d) \to J \in Comp)$
132	131	imp	$⊢ (J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)) \to J \in Comp$
133	132	exlimiv	$⊢ \exists x (J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)) \to J \in Comp$
134	2 133	impbii	$⊢ J \in Comp \leftrightarrow \exists x (J = topGen (fi (x)) \land \forall c \in 𝒫 x (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$

Metamath Proof Explorer

Theorem alexsubALT

Proof