Metamath Proof Explorer

Theorem opnmblALT

Description: All open sets are measurable. This alternative proof of opnmbl is significantly shorter, at the expense of invoking countable choice ax-cc . (This was also the original proof before the current opnmbl was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion opnmblALT 
|- ( A e. ( topGen ` ran (,) ) -> A e. dom vol )

Proof

Step Hyp Ref Expression
1 qtopbas 
 |-  ( (,) " ( QQ X. QQ ) ) e. TopBases
2 eltg3 
 |-  ( ( (,) " ( QQ X. QQ ) ) e. TopBases -> ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> E. x ( x C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. x ) ) )
3 1 2 ax-mp 
 |-  ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> E. x ( x C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. x ) )
4 uniiun 
 |-  U. x = U_ y e. x y
5 ssdomg 
 |-  ( ( (,) " ( QQ X. QQ ) ) e. TopBases -> ( x C_ ( (,) " ( QQ X. QQ ) ) -> x ~<_ ( (,) " ( QQ X. QQ ) ) ) )
6 1 5 ax-mp 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> x ~<_ ( (,) " ( QQ X. QQ ) ) )
7 omelon 
 |-  _om e. On
8 qnnen 
 |-  QQ ~~ NN
9 xpen 
 |-  ( ( QQ ~~ NN /\ QQ ~~ NN ) -> ( QQ X. QQ ) ~~ ( NN X. NN ) )
10 8 8 9 mp2an 
 |-  ( QQ X. QQ ) ~~ ( NN X. NN )
11 xpnnen 
 |-  ( NN X. NN ) ~~ NN
12 10 11 entri 
 |-  ( QQ X. QQ ) ~~ NN
13 nnenom 
 |-  NN ~~ _om
14 12 13 entr2i 
 |-  _om ~~ ( QQ X. QQ )
15 isnumi 
 |-  ( ( _om e. On /\ _om ~~ ( QQ X. QQ ) ) -> ( QQ X. QQ ) e. dom card )
16 7 14 15 mp2an 
 |-  ( QQ X. QQ ) e. dom card
17 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
18 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
19 17 18 ax-mp 
 |-  Fun (,)
20 qssre 
 |-  QQ C_ RR
21 ressxr 
 |-  RR C_ RR*
22 20 21 sstri 
 |-  QQ C_ RR*
23 xpss12 
 |-  ( ( QQ C_ RR* /\ QQ C_ RR* ) -> ( QQ X. QQ ) C_ ( RR* X. RR* ) )
24 22 22 23 mp2an 
 |-  ( QQ X. QQ ) C_ ( RR* X. RR* )
25 17 fdmi 
 |-  dom (,) = ( RR* X. RR* )
26 24 25 sseqtrri 
 |-  ( QQ X. QQ ) C_ dom (,)
27 fores 
 |-  ( ( Fun (,) /\ ( QQ X. QQ ) C_ dom (,) ) -> ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) )
28 19 26 27 mp2an 
 |-  ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) )
29 fodomnum 
 |-  ( ( QQ X. QQ ) e. dom card -> ( ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) -> ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) ) )
30 16 28 29 mp2 
 |-  ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ )
31 domentr 
 |-  ( ( ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) /\ ( QQ X. QQ ) ~~ NN ) -> ( (,) " ( QQ X. QQ ) ) ~<_ NN )
32 30 12 31 mp2an 
 |-  ( (,) " ( QQ X. QQ ) ) ~<_ NN
33 domtr 
 |-  ( ( x ~<_ ( (,) " ( QQ X. QQ ) ) /\ ( (,) " ( QQ X. QQ ) ) ~<_ NN ) -> x ~<_ NN )
34 6 32 33 sylancl 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> x ~<_ NN )
35 imassrn 
 |-  ( (,) " ( QQ X. QQ ) ) C_ ran (,)
36 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
37 17 36 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
38 ioombl 
 |-  ( x (,) y ) e. dom vol
39 38 rgen2w 
 |-  A. x e. RR* A. y e. RR* ( x (,) y ) e. dom vol
40 ffnov 
 |-  ( (,) : ( RR* X. RR* ) --> dom vol <-> ( (,) Fn ( RR* X. RR* ) /\ A. x e. RR* A. y e. RR* ( x (,) y ) e. dom vol ) )
41 37 39 40 mpbir2an 
 |-  (,) : ( RR* X. RR* ) --> dom vol
42 frn 
 |-  ( (,) : ( RR* X. RR* ) --> dom vol -> ran (,) C_ dom vol )
43 41 42 ax-mp 
 |-  ran (,) C_ dom vol
44 35 43 sstri 
 |-  ( (,) " ( QQ X. QQ ) ) C_ dom vol
45 sstr 
 |-  ( ( x C_ ( (,) " ( QQ X. QQ ) ) /\ ( (,) " ( QQ X. QQ ) ) C_ dom vol ) -> x C_ dom vol )
46 44 45 mpan2 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> x C_ dom vol )
47 dfss3 
 |-  ( x C_ dom vol <-> A. y e. x y e. dom vol )
48 46 47 sylib 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> A. y e. x y e. dom vol )
49 iunmbl2 
 |-  ( ( x ~<_ NN /\ A. y e. x y e. dom vol ) -> U_ y e. x y e. dom vol )
50 34 48 49 syl2anc 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> U_ y e. x y e. dom vol )
51 4 50 eqeltrid 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> U. x e. dom vol )
52 eleq1 
 |-  ( A = U. x -> ( A e. dom vol <-> U. x e. dom vol ) )
53 51 52 syl5ibrcom 
 |-  ( x C_ ( (,) " ( QQ X. QQ ) ) -> ( A = U. x -> A e. dom vol ) )
54 53 imp 
 |-  ( ( x C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. x ) -> A e. dom vol )
55 54 exlimiv 
 |-  ( E. x ( x C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. x ) -> A e. dom vol )
56 3 55 sylbi 
 |-  ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) -> A e. dom vol )
57 eqid 
 |-  ( topGen ` ( (,) " ( QQ X. QQ ) ) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
58 57 tgqioo 
 |-  ( topGen ` ran (,) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
59 56 58 eleq2s 
 |-  ( A e. ( topGen ` ran (,) ) -> A e. dom vol )