cmpcref

Description: Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

		Ref	Expression
	Assertion	cmpcref	$⊢ Comp = CovHasRef Fin$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ z = x \to (z Ref y \leftrightarrow x Ref y)$
2		simplr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in (𝒫 y \cap Fin)$
3	2	elin1d	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in 𝒫 y$
4	3	elpwid	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \subseteq y$
5		elpwi	$⊢ y \in 𝒫 j \to y \subseteq j$
6	5	ad4antlr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to y \subseteq j$
7	4 6	sstrd	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \subseteq j$
8		velpw	$⊢ x \in 𝒫 j \leftrightarrow x \subseteq j$
9	7 8	sylibr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in 𝒫 j$
10	2	elin2d	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in Fin$
11	9 10	elind	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in (𝒫 j \cap Fin)$
12		simpr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to ⋃ j = ⋃ x$
13		simpllr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to ⋃ j = ⋃ y$
14	12 13	eqtr3d	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to ⋃ x = ⋃ y$
15		eqid	$⊢ ⋃ x = ⋃ x$
16		eqid	$⊢ ⋃ y = ⋃ y$
17	15 16	ssref	$⊢ (x \in 𝒫 j \land x \subseteq y \land ⋃ x = ⋃ y) \to x Ref y$
18	9 4 14 17	syl3anc	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x Ref y$
19	1 11 18	rspcedvdw	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to \exists z \in (𝒫 j \cap Fin) z Ref y$
20	19	r19.29an	$⊢ (((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x) \to \exists z \in (𝒫 j \cap Fin) z Ref y$
21		simplr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to z \in (𝒫 j \cap Fin)$
22		vex	$⊢ y \in V$
23	22	a1i	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to y \in V$
24		eqid	$⊢ ⋃ z = ⋃ z$
25	24 16	isref	$⊢ z \in V \to (z Ref y \leftrightarrow (⋃ y = ⋃ z \land \forall u \in z \exists v \in y u \subseteq v))$
26	25	elv	$⊢ z Ref y \leftrightarrow (⋃ y = ⋃ z \land \forall u \in z \exists v \in y u \subseteq v)$
27	26	simprbi	$⊢ z Ref y \to \forall u \in z \exists v \in y u \subseteq v$
28	27	adantl	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to \forall u \in z \exists v \in y u \subseteq v$
29		sseq2	$⊢ v = f (u) \to (u \subseteq v \leftrightarrow u \subseteq f (u))$
30	29	ac6	$⊢ (z \in (𝒫 j \cap Fin) \land y \in V \land \forall u \in z \exists v \in y u \subseteq v) \to \exists f (f : z ⟶ y \land \forall u \in z u \subseteq f (u))$
31	21 23 28 30	syl3anc	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to \exists f (f : z ⟶ y \land \forall u \in z u \subseteq f (u))$
32		simplr	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to f : z ⟶ y$
33	32	ffnd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to f Fn z$
34		elinel2	$⊢ z \in (𝒫 j \cap Fin) \to z \in Fin$
35	34	ad4antlr	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to z \in Fin$
36		fnfi	$⊢ (f Fn z \land z \in Fin) \to f \in Fin$
37	33 35 36	syl2anc	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to f \in Fin$
38		rnfi	$⊢ f \in Fin \to ran f \in Fin$
39	37 38	syl	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ran f \in Fin$
40	32	frnd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ran f \subseteq y$
41	39 40	elpwd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ran f \in 𝒫 y$
42	41 39	elind	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ran f \in (𝒫 y \cap Fin)$
43		simp-5r	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ j = ⋃ y$
44	24 16	refbas	$⊢ z Ref y \to ⋃ y = ⋃ z$
45	44	ad3antlr	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ y = ⋃ z$
46		nfv	$⊢ Ⅎ u (((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y)$
47		nfra1	$⊢ Ⅎ u \forall u \in z u \subseteq f (u)$
48	46 47	nfan	$⊢ Ⅎ u ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u))$
49		rspa	$⊢ (\forall u \in z u \subseteq f (u) \land u \in z) \to u \subseteq f (u)$
50	49	adantll	$⊢ (((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \land u \in z) \to u \subseteq f (u)$
51	50	sseld	$⊢ (((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \land u \in z) \to (x \in u \to x \in f (u))$
52	51	ex	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to (u \in z \to (x \in u \to x \in f (u)))$
53	48 52	reximdai	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to (\exists u \in z x \in u \to \exists u \in z x \in f (u))$
54		eluni2	$⊢ x \in ⋃ z \leftrightarrow \exists u \in z x \in u$
55	54	a1i	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to (x \in ⋃ z \leftrightarrow \exists u \in z x \in u)$
56		fnunirn	$⊢ f Fn z \to (x \in ⋃ ran f \leftrightarrow \exists u \in z x \in f (u))$
57	33 56	syl	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to (x \in ⋃ ran f \leftrightarrow \exists u \in z x \in f (u))$
58	53 55 57	3imtr4d	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to (x \in ⋃ z \to x \in ⋃ ran f)$
59	58	ssrdv	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ z \subseteq ⋃ ran f$
60	45 59	eqsstrd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ y \subseteq ⋃ ran f$
61	40	unissd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ ran f \subseteq ⋃ y$
62	60 61	eqssd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ y = ⋃ ran f$
63	43 62	eqtrd	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to ⋃ j = ⋃ ran f$
64		unieq	$⊢ x = ran f \to ⋃ x = ⋃ ran f$
65	64	rspceeqv	$⊢ (ran f \in (𝒫 y \cap Fin) \land ⋃ j = ⋃ ran f) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x$
66	42 63 65	syl2anc	$⊢ ((((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \land f : z ⟶ y) \land \forall u \in z u \subseteq f (u)) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x$
67	66	expl	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to ((f : z ⟶ y \land \forall u \in z u \subseteq f (u)) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x)$
68	67	exlimdv	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to (\exists f (f : z ⟶ y \land \forall u \in z u \subseteq f (u)) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x)$
69	31 68	mpd	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land z \in (𝒫 j \cap Fin)) \land z Ref y) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x$
70	69	r19.29an	$⊢ (((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land \exists z \in (𝒫 j \cap Fin) z Ref y) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x$
71	20 70	impbida	$⊢ ((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \to (\exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x \leftrightarrow \exists z \in (𝒫 j \cap Fin) z Ref y)$
72	71	pm5.74da	$⊢ (j \in Top \land y \in 𝒫 j) \to ((⋃ j = ⋃ y \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x) \leftrightarrow (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap Fin) z Ref y))$
73	72	ralbidva	$⊢ j \in Top \to (\forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x) \leftrightarrow \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap Fin) z Ref y))$
74	73	pm5.32i	$⊢ (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x)) \leftrightarrow (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap Fin) z Ref y))$
75		eqid	$⊢ ⋃ j = ⋃ j$
76	75	iscmp	$⊢ j \in Comp \leftrightarrow (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x))$
77	75	iscref	$⊢ j \in CovHasRef Fin \leftrightarrow (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap Fin) z Ref y))$
78	74 76 77	3bitr4i	$⊢ j \in Comp \leftrightarrow j \in CovHasRef Fin$
79	78	eqriv	$⊢ Comp = CovHasRef Fin$

Metamath Proof Explorer

Theorem cmpcref

Proof