Theorem 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	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ) → 𝐴 ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
2	1	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
3		undif2	⊢ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = ( { ∅ } ∪ 𝐴 )
4		omex	⊢ ω ∈ V
5		peano1	⊢ ∅ ∈ ω
6		snssi	⊢ ( ∅ ∈ ω → { ∅ } ⊆ ω )
7	5 6	ax-mp	⊢ { ∅ } ⊆ ω
8		ssdomg	⊢ ( ω ∈ V → ( { ∅ } ⊆ ω → { ∅ } ≼ ω ) )
9	4 7 8	mp2	⊢ { ∅ } ≼ ω
10		id	⊢ ( 𝐽 ∈ 2ndω → 𝐽 ∈ 2ndω )
11		ssdif	⊢ ( 𝐴 ⊆ 𝐽 → ( 𝐴 ∖ { ∅ } ) ⊆ ( 𝐽 ∖ { ∅ } ) )
12		dfss3	⊢ ( ( 𝐴 ∖ { ∅ } ) ⊆ ( 𝐽 ∖ { ∅ } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑥 ∈ ( 𝐽 ∖ { ∅ } ) )
13	11 12	sylib	⊢ ( 𝐴 ⊆ 𝐽 → ∀ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑥 ∈ ( 𝐽 ∖ { ∅ } ) )
14		eldifi	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) → 𝑥 ∈ 𝐴 )
15	14	anim1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
16	15	moimi	⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) )
17	16	alimi	⊢ ( ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) )
18		df-rmo	⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑦 ∈ 𝑥 ↔ ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) )
19	18	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) )
20		2ndcdisj	⊢ ( ( 𝐽 ∈ 2ndω ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑥 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑦 ∈ 𝑥 ) → ( 𝐴 ∖ { ∅ } ) ≼ ω )
21	19 20	syl3an3br	⊢ ( ( 𝐽 ∈ 2ndω ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) 𝑥 ∈ ( 𝐽 ∖ { ∅ } ) ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐴 ∖ { ∅ } ) ≼ ω )
22	10 13 17 21	syl3an	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐴 ∖ { ∅ } ) ≼ ω )
23		unctb	⊢ ( ( { ∅ } ≼ ω ∧ ( 𝐴 ∖ { ∅ } ) ≼ ω ) → ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) ≼ ω )
24	9 22 23	sylancr	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) ≼ ω )
25	3 24	eqbrtrrid	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( { ∅ } ∪ 𝐴 ) ≼ ω )
26		ctex	⊢ ( ( { ∅ } ∪ 𝐴 ) ≼ ω → ( { ∅ } ∪ 𝐴 ) ∈ V )
27	25 26	syl	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( { ∅ } ∪ 𝐴 ) ∈ V )
28		ssun2	⊢ 𝐴 ⊆ ( { ∅ } ∪ 𝐴 )
29		ssdomg	⊢ ( ( { ∅ } ∪ 𝐴 ) ∈ V → ( 𝐴 ⊆ ( { ∅ } ∪ 𝐴 ) → 𝐴 ≼ ( { ∅ } ∪ 𝐴 ) ) )
30	27 28 29	mpisyl	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐴 ≼ ( { ∅ } ∪ 𝐴 ) )
31		domtr	⊢ ( ( 𝐴 ≼ ( { ∅ } ∪ 𝐴 ) ∧ ( { ∅ } ∪ 𝐴 ) ≼ ω ) → 𝐴 ≼ ω )
32	30 25 31	syl2anc	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐴 ≼ ω )
33	2 32	syl3an3b	⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ) → 𝐴 ≼ ω )