This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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