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)

		Ref	Expression
	Assertion	cmpcref	$⊢ Comp = CovHasRef Fin$

Proof

Step	Hyp	Ref	Expression
1		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)$
2		elin	$⊢ x \in (𝒫 y \cap Fin) \leftrightarrow (x \in 𝒫 y \land x \in Fin)$
3	1 2	sylib	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to (x \in 𝒫 y \land x \in Fin)$
4	3	simpld	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in 𝒫 y$
5		elpwi	$⊢ x \in 𝒫 y \to x \subseteq y$
6	4 5	syl	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \subseteq y$
7		elpwi	$⊢ y \in 𝒫 j \to y \subseteq j$
8	7	ad4antlr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to y \subseteq j$
9	6 8	sstrd	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \subseteq j$
10		velpw	$⊢ x \in 𝒫 j \leftrightarrow x \subseteq j$
11	9 10	sylibr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in 𝒫 j$
12	3	simprd	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x \in Fin$
13	11 12	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)$
14		simpr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to ⋃ j = ⋃ x$
15		simpllr	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to ⋃ j = ⋃ y$
16	14 15	eqtr3d	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to ⋃ x = ⋃ y$
17		eqid	$⊢ ⋃ x = ⋃ x$
18		eqid	$⊢ ⋃ y = ⋃ y$
19	17 18	ssref	$⊢ (x \in 𝒫 j \land x \subseteq y \land ⋃ x = ⋃ y) \to x Ref y$
20	11 6 16 19	syl3anc	$⊢ ((((j \in Top \land y \in 𝒫 j) \land ⋃ j = ⋃ y) \land x \in (𝒫 y \cap Fin)) \land ⋃ j = ⋃ x) \to x Ref y$
21		breq1	$⊢ z = x \to (z Ref y \leftrightarrow x Ref y)$
22	21	rspcev	$⊢ (x \in (𝒫 j \cap Fin) \land x Ref y) \to \exists z \in (𝒫 j \cap Fin) z Ref y$
23	13 20 22	syl2anc	$⊢ ((((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$
24	23	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$
25		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)$
26		vex	$⊢ z \in V$
27		eqid	$⊢ ⋃ z = ⋃ z$
28	27 18	isref	$⊢ z \in V \to (z Ref y \leftrightarrow (⋃ y = ⋃ z \land \forall u \in z \exists v \in y u \subseteq v))$
29	26 28	ax-mp	$⊢ z Ref y \leftrightarrow (⋃ y = ⋃ z \land \forall u \in z \exists v \in y u \subseteq v)$
30	29	simprbi	$⊢ z Ref y \to \forall u \in z \exists v \in y u \subseteq v$
31	30	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$
32		sseq2	$⊢ v = f (u) \to (u \subseteq v \leftrightarrow u \subseteq f (u))$
33	32	ac6sg	$⊢ z \in (𝒫 j \cap Fin) \to (\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)))$
34	25 31 33	sylc	$⊢ ((((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))$
35		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$
36	35	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$
37		vex	$⊢ f \in V$
38	37	rnex	$⊢ ran f \in V$
39	38	elpw	$⊢ ran f \in 𝒫 y \leftrightarrow ran f \subseteq y$
40	36 39	sylibr	$⊢ ((((((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$
41	35	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$
42		elin	$⊢ z \in (𝒫 j \cap Fin) \leftrightarrow (z \in 𝒫 j \land z \in Fin)$
43	42	simprbi	$⊢ z \in (𝒫 j \cap Fin) \to z \in Fin$
44	43	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$
45		fnfi	$⊢ (f Fn z \land z \in Fin) \to f \in Fin$
46	41 44 45	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$
47		rnfi	$⊢ f \in Fin \to ran f \in Fin$
48	46 47	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$
49	40 48	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)$
50		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$
51	27 18	refbas	$⊢ z Ref y \to ⋃ y = ⋃ z$
52	51	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$
53		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)$
54		nfra1	$⊢ Ⅎ u \forall u \in z u \subseteq f (u)$
55	53 54	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))$
56		rspa	$⊢ (\forall u \in z u \subseteq f (u) \land u \in z) \to u \subseteq f (u)$
57	56	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)$
58	57	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))$
59	58	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)))$
60	55 59	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))$
61		eluni2	$⊢ x \in ⋃ z \leftrightarrow \exists u \in z x \in u$
62	61	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)$
63		fnunirn	$⊢ f Fn z \to (x \in ⋃ ran f \leftrightarrow \exists u \in z x \in f (u))$
64	41 63	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))$
65	60 62 64	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)$
66	65	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$
67	52 66	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$
68	36	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$
69	67 68	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$
70	50 69	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$
71		unieq	$⊢ x = ran f \to ⋃ x = ⋃ ran f$
72	71	rspceeqv	$⊢ (ran f \in (𝒫 y \cap Fin) \land ⋃ j = ⋃ ran f) \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x$
73	49 70 72	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$
74	73	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)$
75	74	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)$
76	34 75	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$
77	76	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$
78	24 77	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)$
79	78	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))$
80	79	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))$
81	80	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))$
82		eqid	$⊢ ⋃ j = ⋃ j$
83	82	iscmp	$⊢ j \in Comp \leftrightarrow (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists x \in (𝒫 y \cap Fin) ⋃ j = ⋃ x))$
84	82	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))$
85	81 83 84	3bitr4i	$⊢ j \in Comp \leftrightarrow j \in CovHasRef Fin$
86	85	eqriv	$⊢ Comp = CovHasRef Fin$

Metamath Proof Explorer

Theorem cmpcref

Proof