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 )