comppfsc

Description: A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypothesis	comppfsc.1	$⊢ X = ⋃ J$
	Assertion	comppfsc	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)))$

Proof

Step	Hyp	Ref	Expression
1		comppfsc.1	$⊢ X = ⋃ J$
2		elpwi	$⊢ c \in 𝒫 J \to c \subseteq J$
3	1	cmpcov	$⊢ (J \in Comp \land c \subseteq J \land X = ⋃ c) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d$
4		elfpw	$⊢ d \in (𝒫 c \cap Fin) \leftrightarrow (d \subseteq c \land d \in Fin)$
5		finptfin	$⊢ d \in Fin \to d \in PtFin$
6	5	anim1i	$⊢ (d \in Fin \land (d \subseteq c \land X = ⋃ d)) \to (d \in PtFin \land (d \subseteq c \land X = ⋃ d))$
7	6	anassrs	$⊢ ((d \in Fin \land d \subseteq c) \land X = ⋃ d) \to (d \in PtFin \land (d \subseteq c \land X = ⋃ d))$
8	7	ancom1s	$⊢ ((d \subseteq c \land d \in Fin) \land X = ⋃ d) \to (d \in PtFin \land (d \subseteq c \land X = ⋃ d))$
9	4 8	sylanb	$⊢ (d \in (𝒫 c \cap Fin) \land X = ⋃ d) \to (d \in PtFin \land (d \subseteq c \land X = ⋃ d))$
10	9	reximi2	$⊢ \exists d \in (𝒫 c \cap Fin) X = ⋃ d \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)$
11	3 10	syl	$⊢ (J \in Comp \land c \subseteq J \land X = ⋃ c) \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)$
12	11	3exp	$⊢ J \in Comp \to (c \subseteq J \to (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)))$
13	2 12	syl5	$⊢ J \in Comp \to (c \in 𝒫 J \to (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)))$
14	13	ralrimiv	$⊢ J \in Comp \to \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d))$
15		elpwi	$⊢ a \in 𝒫 J \to a \subseteq J$
16		0elpw	$⊢ \emptyset \in 𝒫 a$
17		0fin	$⊢ \emptyset \in Fin$
18	16 17	elini	$⊢ \emptyset \in (𝒫 a \cap Fin)$
19		unieq	$⊢ b = \emptyset \to ⋃ b = ⋃ \emptyset$
20		uni0	$⊢ ⋃ \emptyset = \emptyset$
21	19 20	eqtrdi	$⊢ b = \emptyset \to ⋃ b = \emptyset$
22	21	rspceeqv	$⊢ (\emptyset \in (𝒫 a \cap Fin) \land X = \emptyset) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b$
23	18 22	mpan	$⊢ X = \emptyset \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b$
24	23	a1i13	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (X = \emptyset \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
25		n0	$⊢ X \neq \emptyset \leftrightarrow \exists x x \in X$
26		simp2	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to X = ⋃ a$
27	26	eleq2d	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (x \in X \leftrightarrow x \in ⋃ a)$
28	27	biimpd	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (x \in X \to x \in ⋃ a)$
29		eluni2	$⊢ x \in ⋃ a \leftrightarrow \exists s \in a x \in s$
30	28 29	syl6ib	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (x \in X \to \exists s \in a x \in s)$
31		simpl3	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to a \subseteq J$
32		simprl	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to s \in a$
33	31 32	sseldd	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to s \in J$
34		elssuni	$⊢ s \in J \to s \subseteq ⋃ J$
35	34 1	sseqtrrdi	$⊢ s \in J \to s \subseteq X$
36	33 35	syl	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to s \subseteq X$
37	36	ralrimivw	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to \forall p \in a s \subseteq X$
38		iunss	$⊢ ⋃_{p \in a} s \subseteq X \leftrightarrow \forall p \in a s \subseteq X$
39	37 38	sylibr	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to ⋃_{p \in a} s \subseteq X$
40		ssequn1	$⊢ ⋃_{p \in a} s \subseteq X \leftrightarrow ⋃_{p \in a} s \cup X = X$
41	39 40	sylib	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to ⋃_{p \in a} s \cup X = X$
42		simpl2	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to X = ⋃ a$
43		uniiun	$⊢ ⋃ a = ⋃_{p \in a} p$
44	42 43	eqtrdi	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to X = ⋃_{p \in a} p$
45	44	uneq2d	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to ⋃_{p \in a} s \cup X = ⋃_{p \in a} s \cup ⋃_{p \in a} p$
46	41 45	eqtr3d	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to X = ⋃_{p \in a} s \cup ⋃_{p \in a} p$
47		iunun	$⊢ ⋃_{p \in a} (s \cup p) = ⋃_{p \in a} s \cup ⋃_{p \in a} p$
48		vex	$⊢ s \in V$
49		vex	$⊢ p \in V$
50	48 49	unex	$⊢ s \cup p \in V$
51	50	dfiun3	$⊢ ⋃_{p \in a} (s \cup p) = ⋃ ran (p \in a ⟼ s \cup p)$
52	47 51	eqtr3i	$⊢ ⋃_{p \in a} s \cup ⋃_{p \in a} p = ⋃ ran (p \in a ⟼ s \cup p)$
53	46 52	eqtrdi	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to X = ⋃ ran (p \in a ⟼ s \cup p)$
54		simpll1	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land p \in a) \to J \in Top$
55	33	adantr	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land p \in a) \to s \in J$
56	31	sselda	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land p \in a) \to p \in J$
57		unopn	$⊢ (J \in Top \land s \in J \land p \in J) \to s \cup p \in J$
58	54 55 56 57	syl3anc	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land p \in a) \to s \cup p \in J$
59	58	fmpttd	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (p \in a ⟼ s \cup p) : a ⟶ J$
60	59	frnd	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to ran (p \in a ⟼ s \cup p) \subseteq J$
61		elpw2g	$⊢ J \in Top \to (ran (p \in a ⟼ s \cup p) \in 𝒫 J \leftrightarrow ran (p \in a ⟼ s \cup p) \subseteq J)$
62	61	3ad2ant1	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (ran (p \in a ⟼ s \cup p) \in 𝒫 J \leftrightarrow ran (p \in a ⟼ s \cup p) \subseteq J)$
63	62	adantr	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (ran (p \in a ⟼ s \cup p) \in 𝒫 J \leftrightarrow ran (p \in a ⟼ s \cup p) \subseteq J)$
64	60 63	mpbird	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to ran (p \in a ⟼ s \cup p) \in 𝒫 J$
65		unieq	$⊢ c = ran (p \in a ⟼ s \cup p) \to ⋃ c = ⋃ ran (p \in a ⟼ s \cup p)$
66	65	eqeq2d	$⊢ c = ran (p \in a ⟼ s \cup p) \to (X = ⋃ c \leftrightarrow X = ⋃ ran (p \in a ⟼ s \cup p))$
67		sseq2	$⊢ c = ran (p \in a ⟼ s \cup p) \to (d \subseteq c \leftrightarrow d \subseteq ran (p \in a ⟼ s \cup p))$
68	67	anbi1d	$⊢ c = ran (p \in a ⟼ s \cup p) \to ((d \subseteq c \land X = ⋃ d) \leftrightarrow (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d))$
69	68	rexbidv	$⊢ c = ran (p \in a ⟼ s \cup p) \to (\exists d \in PtFin (d \subseteq c \land X = ⋃ d) \leftrightarrow \exists d \in PtFin (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d))$
70	66 69	imbi12d	$⊢ c = ran (p \in a ⟼ s \cup p) \to ((X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \leftrightarrow (X = ⋃ ran (p \in a ⟼ s \cup p) \to \exists d \in PtFin (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)))$
71	70	rspcv	$⊢ ran (p \in a ⟼ s \cup p) \in 𝒫 J \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to (X = ⋃ ran (p \in a ⟼ s \cup p) \to \exists d \in PtFin (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)))$
72	64 71	syl	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to (X = ⋃ ran (p \in a ⟼ s \cup p) \to \exists d \in PtFin (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)))$
73	53 72	mpid	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists d \in PtFin (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d))$
74		simprr	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to x \in s$
75		ssel2	$⊢ (a \subseteq J \land s \in a) \to s \in J$
76	75	3ad2antl3	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land s \in a) \to s \in J$
77	76	adantrr	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to s \in J$
78		elunii	$⊢ (x \in s \land s \in J) \to x \in ⋃ J$
79	74 77 78	syl2anc	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to x \in ⋃ J$
80	79 1	eleqtrrdi	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to x \in X$
81	80	adantr	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to x \in X$
82		simprr	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to X = ⋃ d$
83	81 82	eleqtrd	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to x \in ⋃ d$
84		eqid	$⊢ ⋃ d = ⋃ d$
85	84	ptfinfin	$⊢ (d \in PtFin \land x \in ⋃ d) \to \{z \in d \| x \in z\} \in Fin$
86	85	expcom	$⊢ x \in ⋃ d \to (d \in PtFin \to \{z \in d \| x \in z\} \in Fin)$
87	83 86	syl	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (d \in PtFin \to \{z \in d \| x \in z\} \in Fin)$
88		simprl	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to d \subseteq ran (p \in a ⟼ s \cup p)$
89		elun1	$⊢ x \in s \to x \in (s \cup p)$
90	89	ad2antll	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to x \in (s \cup p)$
91	90	ralrimivw	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to \forall p \in a x \in (s \cup p)$
92	50	rgenw	$⊢ \forall p \in a s \cup p \in V$
93		eqid	$⊢ (p \in a ⟼ s \cup p) = (p \in a ⟼ s \cup p)$
94		eleq2	$⊢ z = s \cup p \to (x \in z \leftrightarrow x \in (s \cup p))$
95	93 94	ralrnmptw	$⊢ \forall p \in a s \cup p \in V \to (\forall z \in ran (p \in a ⟼ s \cup p) x \in z \leftrightarrow \forall p \in a x \in (s \cup p))$
96	92 95	ax-mp	$⊢ \forall z \in ran (p \in a ⟼ s \cup p) x \in z \leftrightarrow \forall p \in a x \in (s \cup p)$
97	91 96	sylibr	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to \forall z \in ran (p \in a ⟼ s \cup p) x \in z$
98	97	adantr	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to \forall z \in ran (p \in a ⟼ s \cup p) x \in z$
99		ssralv	$⊢ d \subseteq ran (p \in a ⟼ s \cup p) \to (\forall z \in ran (p \in a ⟼ s \cup p) x \in z \to \forall z \in d x \in z)$
100	88 98 99	sylc	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to \forall z \in d x \in z$
101		rabid2	$⊢ d = \{z \in d \| x \in z\} \leftrightarrow \forall z \in d x \in z$
102	100 101	sylibr	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to d = \{z \in d \| x \in z\}$
103	102	eleq1d	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (d \in Fin \leftrightarrow \{z \in d \| x \in z\} \in Fin)$
104	103	biimprd	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (\{z \in d \| x \in z\} \in Fin \to d \in Fin)$
105	93	rnmpt	$⊢ ran (p \in a ⟼ s \cup p) = \{q \| \exists p \in a q = s \cup p\}$
106	88 105	sseqtrdi	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to d \subseteq \{q \| \exists p \in a q = s \cup p\}$
107		ssabral	$⊢ d \subseteq \{q \| \exists p \in a q = s \cup p\} \leftrightarrow \forall q \in d \exists p \in a q = s \cup p$
108	106 107	sylib	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to \forall q \in d \exists p \in a q = s \cup p$
109		uneq2	$⊢ p = f (q) \to s \cup p = s \cup f (q)$
110	109	eqeq2d	$⊢ p = f (q) \to (q = s \cup p \leftrightarrow q = s \cup f (q))$
111	110	ac6sfi	$⊢ (d \in Fin \land \forall q \in d \exists p \in a q = s \cup p) \to \exists f (f : d ⟶ a \land \forall q \in d q = s \cup f (q))$
112	111	expcom	$⊢ \forall q \in d \exists p \in a q = s \cup p \to (d \in Fin \to \exists f (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))$
113	108 112	syl	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (d \in Fin \to \exists f (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))$
114		frn	$⊢ f : d ⟶ a \to ran f \subseteq a$
115	114	adantr	$⊢ (f : d ⟶ a \land \forall q \in d q = s \cup f (q)) \to ran f \subseteq a$
116	115	ad2antll	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \subseteq a$
117	32	ad2antrr	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to s \in a$
118	117	snssd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to \{s\} \subseteq a$
119	116 118	unssd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \cup \{s\} \subseteq a$
120		simprl	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to d \in Fin$
121		simprrl	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to f : d ⟶ a$
122	121	ffnd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to f Fn d$
123		dffn4	$⊢ f Fn d \leftrightarrow f : d \underset{onto}{⟶} ran f$
124	122 123	sylib	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to f : d \underset{onto}{⟶} ran f$
125		fofi	$⊢ (d \in Fin \land f : d \underset{onto}{⟶} ran f) \to ran f \in Fin$
126	120 124 125	syl2anc	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \in Fin$
127		snfi	$⊢ \{s\} \in Fin$
128		unfi	$⊢ (ran f \in Fin \land \{s\} \in Fin) \to ran f \cup \{s\} \in Fin$
129	126 127 128	sylancl	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \cup \{s\} \in Fin$
130		elfpw	$⊢ ran f \cup \{s\} \in (𝒫 a \cap Fin) \leftrightarrow (ran f \cup \{s\} \subseteq a \land ran f \cup \{s\} \in Fin)$
131	119 129 130	sylanbrc	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \cup \{s\} \in (𝒫 a \cap Fin)$
132		simplrr	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to X = ⋃ d$
133		uniiun	$⊢ ⋃ d = ⋃_{q \in d} q$
134		simprrr	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to \forall q \in d q = s \cup f (q)$
135		iuneq2	$⊢ \forall q \in d q = s \cup f (q) \to ⋃_{q \in d} q = ⋃_{q \in d} (s \cup f (q))$
136	134 135	syl	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ⋃_{q \in d} q = ⋃_{q \in d} (s \cup f (q))$
137	133 136	syl5eq	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ⋃ d = ⋃_{q \in d} (s \cup f (q))$
138	132 137	eqtrd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to X = ⋃_{q \in d} (s \cup f (q))$
139		ssun2	$⊢ \{s\} \subseteq ran f \cup \{s\}$
140		vsnid	$⊢ s \in \{s\}$
141	139 140	sselii	$⊢ s \in (ran f \cup \{s\})$
142		elssuni	$⊢ s \in (ran f \cup \{s\}) \to s \subseteq ⋃ (ran f \cup \{s\})$
143	141 142	ax-mp	$⊢ s \subseteq ⋃ (ran f \cup \{s\})$
144		fvssunirn	$⊢ f (q) \subseteq ⋃ ran f$
145		ssun1	$⊢ ran f \subseteq ran f \cup \{s\}$
146	145	unissi	$⊢ ⋃ ran f \subseteq ⋃ (ran f \cup \{s\})$
147	144 146	sstri	$⊢ f (q) \subseteq ⋃ (ran f \cup \{s\})$
148	143 147	unssi	$⊢ s \cup f (q) \subseteq ⋃ (ran f \cup \{s\})$
149	148	rgenw	$⊢ \forall q \in d s \cup f (q) \subseteq ⋃ (ran f \cup \{s\})$
150		iunss	$⊢ ⋃_{q \in d} (s \cup f (q)) \subseteq ⋃ (ran f \cup \{s\}) \leftrightarrow \forall q \in d s \cup f (q) \subseteq ⋃ (ran f \cup \{s\})$
151	149 150	mpbir	$⊢ ⋃_{q \in d} (s \cup f (q)) \subseteq ⋃ (ran f \cup \{s\})$
152	138 151	eqsstrdi	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to X \subseteq ⋃ (ran f \cup \{s\})$
153	31	ad2antrr	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to a \subseteq J$
154	116 153	sstrd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \subseteq J$
155	33	ad2antrr	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to s \in J$
156	155	snssd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to \{s\} \subseteq J$
157	154 156	unssd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ran f \cup \{s\} \subseteq J$
158		uniss	$⊢ ran f \cup \{s\} \subseteq J \to ⋃ (ran f \cup \{s\}) \subseteq ⋃ J$
159	158 1	sseqtrrdi	$⊢ ran f \cup \{s\} \subseteq J \to ⋃ (ran f \cup \{s\}) \subseteq X$
160	157 159	syl	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to ⋃ (ran f \cup \{s\}) \subseteq X$
161	152 160	eqssd	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to X = ⋃ (ran f \cup \{s\})$
162		unieq	$⊢ b = ran f \cup \{s\} \to ⋃ b = ⋃ (ran f \cup \{s\})$
163	162	rspceeqv	$⊢ (ran f \cup \{s\} \in (𝒫 a \cap Fin) \land X = ⋃ (ran f \cup \{s\})) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b$
164	131 161 163	syl2anc	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land (d \in Fin \land (f : d ⟶ a \land \forall q \in d q = s \cup f (q)))) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b$
165	164	expr	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land d \in Fin) \to ((f : d ⟶ a \land \forall q \in d q = s \cup f (q)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
166	165	exlimdv	$⊢ ((((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \land d \in Fin) \to (\exists f (f : d ⟶ a \land \forall q \in d q = s \cup f (q)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
167	166	ex	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (d \in Fin \to (\exists f (f : d ⟶ a \land \forall q \in d q = s \cup f (q)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
168	113 167	mpdd	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (d \in Fin \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
169	87 104 168	3syld	$⊢ (((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \land (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d)) \to (d \in PtFin \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
170	169	ex	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to ((d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d) \to (d \in PtFin \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
171	170	com23	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (d \in PtFin \to ((d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
172	171	rexlimdv	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (\exists d \in PtFin (d \subseteq ran (p \in a ⟼ s \cup p) \land X = ⋃ d) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
173	73 172	syld	$⊢ ((J \in Top \land X = ⋃ a \land a \subseteq J) \land (s \in a \land x \in s)) \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
174	173	rexlimdvaa	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (\exists s \in a x \in s \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
175	30 174	syld	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (x \in X \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
176	175	exlimdv	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (\exists x x \in X \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
177	25 176	syl5bi	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (X \neq \emptyset \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
178	24 177	pm2.61dne	$⊢ (J \in Top \land X = ⋃ a \land a \subseteq J) \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
179	15 178	syl3an3	$⊢ (J \in Top \land X = ⋃ a \land a \in 𝒫 J) \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)$
180	179	3exp	$⊢ J \in Top \to (X = ⋃ a \to (a \in 𝒫 J \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)))$
181	180	com24	$⊢ J \in Top \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to (a \in 𝒫 J \to (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b)))$
182	181	ralrimdv	$⊢ J \in Top \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to \forall a \in 𝒫 J (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
183	1	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall a \in 𝒫 J (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b))$
184	183	baibr	$⊢ J \in Top \to (\forall a \in 𝒫 J (X = ⋃ a \to \exists b \in (𝒫 a \cap Fin) X = ⋃ b) \leftrightarrow J \in Comp)$
185	182 184	sylibd	$⊢ J \in Top \to (\forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)) \to J \in Comp)$
186	14 185	impbid2	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in PtFin (d \subseteq c \land X = ⋃ d)))$

Metamath Proof Explorer

Theorem comppfsc

Proof