2ndcdisj2

Description: Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015) (Proof shortened by Mario Carneiro, 9-Apr-2015) (Revised by NM, 17-Jun-2017)

		Ref	Expression
	Assertion	2ndcdisj2	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x \in A y \in x) \to A ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		df-rmo	$⊢ \exists^{} x \in A y \in x \leftrightarrow \exists^{} x (x \in A \land y \in x)$
2	1	albii	$⊢ \forall y \exists^{} x \in A y \in x \leftrightarrow \forall y \exists^{} x (x \in A \land y \in x)$
3		undif2	$⊢ \{\emptyset\} \cup (A ∖ \{\emptyset\}) = \{\emptyset\} \cup A$
4		omex	$⊢ ω \in V$
5		peano1	$⊢ \emptyset \in ω$
6		snssi	$⊢ \emptyset \in ω \to \{\emptyset\} \subseteq ω$
7	5 6	ax-mp	$⊢ \{\emptyset\} \subseteq ω$
8		ssdomg	$⊢ ω \in V \to (\{\emptyset\} \subseteq ω \to \{\emptyset\} ≼ ω)$
9	4 7 8	mp2	$⊢ \{\emptyset\} ≼ ω$
10		id	$⊢ J \in 2^{nd} 𝜔 \to J \in 2^{nd} 𝜔$
11		ssdif	$⊢ A \subseteq J \to A ∖ \{\emptyset\} \subseteq J ∖ \{\emptyset\}$
12		dfss3	$⊢ A ∖ \{\emptyset\} \subseteq J ∖ \{\emptyset\} \leftrightarrow \forall x \in (A ∖ \{\emptyset\}) x \in (J ∖ \{\emptyset\})$
13	11 12	sylib	$⊢ A \subseteq J \to \forall x \in (A ∖ \{\emptyset\}) x \in (J ∖ \{\emptyset\})$
14		eldifi	$⊢ x \in (A ∖ \{\emptyset\}) \to x \in A$
15	14	anim1i	$⊢ (x \in (A ∖ \{\emptyset\}) \land y \in x) \to (x \in A \land y \in x)$
16	15	moimi	$⊢ \exists^{} x (x \in A \land y \in x) \to \exists^{} x (x \in (A ∖ \{\emptyset\}) \land y \in x)$
17	16	alimi	$⊢ \forall y \exists^{} x (x \in A \land y \in x) \to \forall y \exists^{} x (x \in (A ∖ \{\emptyset\}) \land y \in x)$
18		df-rmo	$⊢ \exists^{} x \in (A ∖ \{\emptyset\}) y \in x \leftrightarrow \exists^{} x (x \in (A ∖ \{\emptyset\}) \land y \in x)$
19	18	albii	$⊢ \forall y \exists^{} x \in (A ∖ \{\emptyset\}) y \in x \leftrightarrow \forall y \exists^{} x (x \in (A ∖ \{\emptyset\}) \land y \in x)$
20		2ndcdisj	$⊢ (J \in 2^{nd} 𝜔 \land \forall x \in (A ∖ \{\emptyset\}) x \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in (A ∖ \{\emptyset\}) y \in x) \to (A ∖ \{\emptyset\}) ≼ ω$
21	19 20	syl3an3br	$⊢ (J \in 2^{nd} 𝜔 \land \forall x \in (A ∖ \{\emptyset\}) x \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x (x \in (A ∖ \{\emptyset\}) \land y \in x)) \to (A ∖ \{\emptyset\}) ≼ ω$
22	10 13 17 21	syl3an	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x (x \in A \land y \in x)) \to (A ∖ \{\emptyset\}) ≼ ω$
23		unctb	$⊢ (\{\emptyset\} ≼ ω \land (A ∖ \{\emptyset\}) ≼ ω) \to (\{\emptyset\} \cup (A ∖ \{\emptyset\})) ≼ ω$
24	9 22 23	sylancr	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x (x \in A \land y \in x)) \to (\{\emptyset\} \cup (A ∖ \{\emptyset\})) ≼ ω$
25	3 24	eqbrtrrid	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x (x \in A \land y \in x)) \to (\{\emptyset\} \cup A) ≼ ω$
26		ctex	$⊢ (\{\emptyset\} \cup A) ≼ ω \to \{\emptyset\} \cup A \in V$
27	25 26	syl	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x (x \in A \land y \in x)) \to \{\emptyset\} \cup A \in V$
28		ssun2	$⊢ A \subseteq \{\emptyset\} \cup A$
29		ssdomg	$⊢ \{\emptyset\} \cup A \in V \to (A \subseteq \{\emptyset\} \cup A \to A ≼ (\{\emptyset\} \cup A))$
30	27 28 29	mpisyl	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x (x \in A \land y \in x)) \to A ≼ (\{\emptyset\} \cup A)$
31		domtr	$⊢ (A ≼ (\{\emptyset\} \cup A) \land (\{\emptyset\} \cup A) ≼ ω) \to A ≼ ω$
32	30 25 31	syl2anc	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x (x \in A \land y \in x)) \to A ≼ ω$
33	2 32	syl3an3b	$⊢ (J \in 2^{nd} 𝜔 \land A \subseteq J \land \forall y \exists^{*} x \in A y \in x) \to A ≼ ω$

Metamath Proof Explorer

Theorem 2ndcdisj2

Proof