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
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x e. A y e. x ) -> A ~<_ _om )

Proof

Step Hyp Ref Expression
1 df-rmo
 |-  ( E* x e. A y e. x <-> E* x ( x e. A /\ y e. x ) )
2 1 albii
 |-  ( A. y E* x e. A y e. x <-> A. y E* x ( x e. A /\ y e. x ) )
3 undif2
 |-  ( { (/) } u. ( A \ { (/) } ) ) = ( { (/) } u. A )
4 omex
 |-  _om e. _V
5 peano1
 |-  (/) e. _om
6 snssi
 |-  ( (/) e. _om -> { (/) } C_ _om )
7 5 6 ax-mp
 |-  { (/) } C_ _om
8 ssdomg
 |-  ( _om e. _V -> ( { (/) } C_ _om -> { (/) } ~<_ _om ) )
9 4 7 8 mp2
 |-  { (/) } ~<_ _om
10 id
 |-  ( J e. 2ndc -> J e. 2ndc )
11 ssdif
 |-  ( A C_ J -> ( A \ { (/) } ) C_ ( J \ { (/) } ) )
12 dfss3
 |-  ( ( A \ { (/) } ) C_ ( J \ { (/) } ) <-> A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) )
13 11 12 sylib
 |-  ( A C_ J -> A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) )
14 eldifi
 |-  ( x e. ( A \ { (/) } ) -> x e. A )
15 14 anim1i
 |-  ( ( x e. ( A \ { (/) } ) /\ y e. x ) -> ( x e. A /\ y e. x ) )
16 15 moimi
 |-  ( E* x ( x e. A /\ y e. x ) -> E* x ( x e. ( A \ { (/) } ) /\ y e. x ) )
17 16 alimi
 |-  ( A. y E* x ( x e. A /\ y e. x ) -> A. y E* x ( x e. ( A \ { (/) } ) /\ y e. x ) )
18 df-rmo
 |-  ( E* x e. ( A \ { (/) } ) y e. x <-> E* x ( x e. ( A \ { (/) } ) /\ y e. x ) )
19 18 albii
 |-  ( A. y E* x e. ( A \ { (/) } ) y e. x <-> A. y E* x ( x e. ( A \ { (/) } ) /\ y e. x ) )
20 2ndcdisj
 |-  ( ( J e. 2ndc /\ A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) /\ A. y E* x e. ( A \ { (/) } ) y e. x ) -> ( A \ { (/) } ) ~<_ _om )
21 19 20 syl3an3br
 |-  ( ( J e. 2ndc /\ A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) /\ A. y E* x ( x e. ( A \ { (/) } ) /\ y e. x ) ) -> ( A \ { (/) } ) ~<_ _om )
22 10 13 17 21 syl3an
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( A \ { (/) } ) ~<_ _om )
23 unctb
 |-  ( ( { (/) } ~<_ _om /\ ( A \ { (/) } ) ~<_ _om ) -> ( { (/) } u. ( A \ { (/) } ) ) ~<_ _om )
24 9 22 23 sylancr
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( { (/) } u. ( A \ { (/) } ) ) ~<_ _om )
25 3 24 eqbrtrrid
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( { (/) } u. A ) ~<_ _om )
26 ctex
 |-  ( ( { (/) } u. A ) ~<_ _om -> ( { (/) } u. A ) e. _V )
27 25 26 syl
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( { (/) } u. A ) e. _V )
28 ssun2
 |-  A C_ ( { (/) } u. A )
29 ssdomg
 |-  ( ( { (/) } u. A ) e. _V -> ( A C_ ( { (/) } u. A ) -> A ~<_ ( { (/) } u. A ) ) )
30 27 28 29 mpisyl
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> A ~<_ ( { (/) } u. A ) )
31 domtr
 |-  ( ( A ~<_ ( { (/) } u. A ) /\ ( { (/) } u. A ) ~<_ _om ) -> A ~<_ _om )
32 30 25 31 syl2anc
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> A ~<_ _om )
33 2 32 syl3an3b
 |-  ( ( J e. 2ndc /\ A C_ J /\ A. y E* x e. A y e. x ) -> A ~<_ _om )