Metamath Proof Explorer

Theorem ovolctb2

Description: The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion ovolctb2 
|- ( ( A C_ RR /\ A ~<_ NN ) -> ( vol* ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. NN )
2 simpl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> A C_ RR )
3 nnssre 
 |-  NN C_ RR
4 unss 
 |-  ( ( A C_ RR /\ NN C_ RR ) <-> ( A u. NN ) C_ RR )
5 2 3 4 sylanblc 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( A u. NN ) C_ RR )
6 nnenom 
 |-  NN ~~ _om
7 domentr 
 |-  ( ( A ~<_ NN /\ NN ~~ _om ) -> A ~<_ _om )
8 6 7 mpan2 
 |-  ( A ~<_ NN -> A ~<_ _om )
9 8 adantl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> A ~<_ _om )
10 nnct 
 |-  NN ~<_ _om
11 unctb 
 |-  ( ( A ~<_ _om /\ NN ~<_ _om ) -> ( A u. NN ) ~<_ _om )
12 9 10 11 sylancl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( A u. NN ) ~<_ _om )
13 6 ensymi 
 |-  _om ~~ NN
14 domentr 
 |-  ( ( ( A u. NN ) ~<_ _om /\ _om ~~ NN ) -> ( A u. NN ) ~<_ NN )
15 12 13 14 sylancl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( A u. NN ) ~<_ NN )
16 reex 
 |-  RR e. _V
17 16 ssex 
 |-  ( ( A u. NN ) C_ RR -> ( A u. NN ) e. _V )
18 5 17 syl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( A u. NN ) e. _V )
19 ssun2 
 |-  NN C_ ( A u. NN )
20 ssdomg 
 |-  ( ( A u. NN ) e. _V -> ( NN C_ ( A u. NN ) -> NN ~<_ ( A u. NN ) ) )
21 18 19 20 mpisyl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> NN ~<_ ( A u. NN ) )
22 sbth 
 |-  ( ( ( A u. NN ) ~<_ NN /\ NN ~<_ ( A u. NN ) ) -> ( A u. NN ) ~~ NN )
23 15 21 22 syl2anc 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( A u. NN ) ~~ NN )
24 ovolctb 
 |-  ( ( ( A u. NN ) C_ RR /\ ( A u. NN ) ~~ NN ) -> ( vol* ` ( A u. NN ) ) = 0 )
25 5 23 24 syl2anc 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( vol* ` ( A u. NN ) ) = 0 )
26 ovolssnul 
 |-  ( ( A C_ ( A u. NN ) /\ ( A u. NN ) C_ RR /\ ( vol* ` ( A u. NN ) ) = 0 ) -> ( vol* ` A ) = 0 )
27 1 5 25 26 mp3an2i 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( vol* ` A ) = 0 )