dissnref

Description: The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)

		Ref	Expression
	Hypothesis	dissnref.c	$⊢ C = \{u \| \exists x \in X u = \{x\}\}$
	Assertion	dissnref	$⊢ (X \in V \land ⋃ Y = X) \to C Ref Y$

Proof

Step	Hyp	Ref	Expression
1		dissnref.c	$⊢ C = \{u \| \exists x \in X u = \{x\}\}$
2		simpr	$⊢ (X \in V \land ⋃ Y = X) \to ⋃ Y = X$
3	1	unisngl	$⊢ X = ⋃ C$
4	2 3	eqtrdi	$⊢ (X \in V \land ⋃ Y = X) \to ⋃ Y = ⋃ C$
5		simplr	$⊢ (((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \land (y \in Y \land x \in y)) \to u = \{x\}$
6		simprr	$⊢ (((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \land (y \in Y \land x \in y)) \to x \in y$
7	6	snssd	$⊢ (((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \land (y \in Y \land x \in y)) \to \{x\} \subseteq y$
8	5 7	eqsstrd	$⊢ (((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \land (y \in Y \land x \in y)) \to u \subseteq y$
9		simplr	$⊢ ((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \to x \in X$
10		simp-4r	$⊢ ((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \to ⋃ Y = X$
11	9 10	eleqtrrd	$⊢ ((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \to x \in ⋃ Y$
12		eluni2	$⊢ x \in ⋃ Y \leftrightarrow \exists y \in Y x \in y$
13	11 12	sylib	$⊢ ((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \to \exists y \in Y x \in y$
14	8 13	reximddv	$⊢ ((((X \in V \land ⋃ Y = X) \land u \in C) \land x \in X) \land u = \{x\}) \to \exists y \in Y u \subseteq y$
15	1	eqabri	$⊢ u \in C \leftrightarrow \exists x \in X u = \{x\}$
16	15	biimpi	$⊢ u \in C \to \exists x \in X u = \{x\}$
17	16	adantl	$⊢ ((X \in V \land ⋃ Y = X) \land u \in C) \to \exists x \in X u = \{x\}$
18	14 17	r19.29a	$⊢ ((X \in V \land ⋃ Y = X) \land u \in C) \to \exists y \in Y u \subseteq y$
19	18	ralrimiva	$⊢ (X \in V \land ⋃ Y = X) \to \forall u \in C \exists y \in Y u \subseteq y$
20		pwexg	$⊢ X \in V \to 𝒫 X \in V$
21		simpr	$⊢ ((u \in C \land x \in X) \land u = \{x\}) \to u = \{x\}$
22		snelpwi	$⊢ x \in X \to \{x\} \in 𝒫 X$
23	22	ad2antlr	$⊢ ((u \in C \land x \in X) \land u = \{x\}) \to \{x\} \in 𝒫 X$
24	21 23	eqeltrd	$⊢ ((u \in C \land x \in X) \land u = \{x\}) \to u \in 𝒫 X$
25	24 16	r19.29a	$⊢ u \in C \to u \in 𝒫 X$
26	25	ssriv	$⊢ C \subseteq 𝒫 X$
27	26	a1i	$⊢ X \in V \to C \subseteq 𝒫 X$
28	20 27	ssexd	$⊢ X \in V \to C \in V$
29	28	adantr	$⊢ (X \in V \land ⋃ Y = X) \to C \in V$
30		eqid	$⊢ ⋃ C = ⋃ C$
31		eqid	$⊢ ⋃ Y = ⋃ Y$
32	30 31	isref	$⊢ C \in V \to (C Ref Y \leftrightarrow (⋃ Y = ⋃ C \land \forall u \in C \exists y \in Y u \subseteq y))$
33	29 32	syl	$⊢ (X \in V \land ⋃ Y = X) \to (C Ref Y \leftrightarrow (⋃ Y = ⋃ C \land \forall u \in C \exists y \in Y u \subseteq y))$
34	4 19 33	mpbir2and	$⊢ (X \in V \land ⋃ Y = X) \to C Ref Y$

Metamath Proof Explorer

Theorem dissnref

Proof