Metamath Proof Explorer

Theorem dyadmbllem

Description: Lemma for dyadmbl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
dyadmbl.2 
|- G = { z e. A | A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) }
dyadmbl.3 
|- ( ph -> A C_ ran F )
Assertion dyadmbllem 
|- ( ph -> U. ( [,] " A ) = U. ( [,] " G ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 dyadmbl.2 
 |-  G = { z e. A | A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) }
3 dyadmbl.3 
 |-  ( ph -> A C_ ran F )
4 eluni2 
 |-  ( a e. U. ( [,] " A ) <-> E. i e. ( [,] " A ) a e. i )
5 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
6 ffn 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> [,] Fn ( RR* X. RR* ) )
7 5 6 ax-mp 
 |-  [,] Fn ( RR* X. RR* )
8 1 dyadf 
 |-  F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
9 frn 
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ ( <_ i^i ( RR X. RR ) ) )
10 8 9 ax-mp 
 |-  ran F C_ ( <_ i^i ( RR X. RR ) )
11 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
12 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
13 11 12 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
14 10 13 sstri 
 |-  ran F C_ ( RR* X. RR* )
15 3 14 sstrdi 
 |-  ( ph -> A C_ ( RR* X. RR* ) )
16 eleq2 
 |-  ( i = ( [,] ` t ) -> ( a e. i <-> a e. ( [,] ` t ) ) )
17 16 rexima 
 |-  ( ( [,] Fn ( RR* X. RR* ) /\ A C_ ( RR* X. RR* ) ) -> ( E. i e. ( [,] " A ) a e. i <-> E. t e. A a e. ( [,] ` t ) ) )
18 7 15 17 sylancr 
 |-  ( ph -> ( E. i e. ( [,] " A ) a e. i <-> E. t e. A a e. ( [,] ` t ) ) )
19 ssrab2 
 |-  { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } C_ A
20 3 adantr 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> A C_ ran F )
21 19 20 sstrid 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } C_ ran F )
22 simprl 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> t e. A )
23 ssid 
 |-  ( [,] ` t ) C_ ( [,] ` t )
24 fveq2 
 |-  ( a = t -> ( [,] ` a ) = ( [,] ` t ) )
25 24 sseq2d 
 |-  ( a = t -> ( ( [,] ` t ) C_ ( [,] ` a ) <-> ( [,] ` t ) C_ ( [,] ` t ) ) )
26 25 rspcev 
 |-  ( ( t e. A /\ ( [,] ` t ) C_ ( [,] ` t ) ) -> E. a e. A ( [,] ` t ) C_ ( [,] ` a ) )
27 22 23 26 sylancl 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> E. a e. A ( [,] ` t ) C_ ( [,] ` a ) )
28 rabn0 
 |-  ( { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } =/= (/) <-> E. a e. A ( [,] ` t ) C_ ( [,] ` a ) )
29 27 28 sylibr 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } =/= (/) )
30 1 dyadmax 
 |-  ( ( { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } C_ ran F /\ { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } =/= (/) ) -> E. m e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) )
31 21 29 30 syl2anc 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> E. m e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) )
32 fveq2 
 |-  ( a = m -> ( [,] ` a ) = ( [,] ` m ) )
33 32 sseq2d 
 |-  ( a = m -> ( ( [,] ` t ) C_ ( [,] ` a ) <-> ( [,] ` t ) C_ ( [,] ` m ) ) )
34 33 elrab 
 |-  ( m e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } <-> ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) )
35 simprlr 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> ( [,] ` t ) C_ ( [,] ` m ) )
36 simplrr 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> a e. ( [,] ` t ) )
37 35 36 sseldd 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> a e. ( [,] ` m ) )
38 simprll 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> m e. A )
39 fveq2 
 |-  ( a = w -> ( [,] ` a ) = ( [,] ` w ) )
40 39 sseq2d 
 |-  ( a = w -> ( ( [,] ` t ) C_ ( [,] ` a ) <-> ( [,] ` t ) C_ ( [,] ` w ) ) )
41 40 elrab 
 |-  ( w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } <-> ( w e. A /\ ( [,] ` t ) C_ ( [,] ` w ) ) )
42 41 imbi1i 
 |-  ( ( w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) <-> ( ( w e. A /\ ( [,] ` t ) C_ ( [,] ` w ) ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
43 impexp 
 |-  ( ( ( w e. A /\ ( [,] ` t ) C_ ( [,] ` w ) ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) <-> ( w e. A -> ( ( [,] ` t ) C_ ( [,] ` w ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) )
44 42 43 bitri 
 |-  ( ( w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) <-> ( w e. A -> ( ( [,] ` t ) C_ ( [,] ` w ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) )
45 impexp 
 |-  ( ( ( ( [,] ` t ) C_ ( [,] ` w ) /\ ( [,] ` m ) C_ ( [,] ` w ) ) -> m = w ) <-> ( ( [,] ` t ) C_ ( [,] ` w ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
46 sstr2 
 |-  ( ( [,] ` t ) C_ ( [,] ` m ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> ( [,] ` t ) C_ ( [,] ` w ) ) )
47 46 ad2antll 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> ( [,] ` t ) C_ ( [,] ` w ) ) )
48 47 ancrd 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> ( ( [,] ` t ) C_ ( [,] ` w ) /\ ( [,] ` m ) C_ ( [,] ` w ) ) ) )
49 48 imim1d 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( ( ( ( [,] ` t ) C_ ( [,] ` w ) /\ ( [,] ` m ) C_ ( [,] ` w ) ) -> m = w ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
50 45 49 syl5bir 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( ( ( [,] ` t ) C_ ( [,] ` w ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
51 50 imim2d 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( ( w e. A -> ( ( [,] ` t ) C_ ( [,] ` w ) -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> ( w e. A -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) )
52 44 51 syl5bi 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( ( w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) -> ( w e. A -> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) )
53 52 ralimdv2 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) ) -> ( A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) -> A. w e. A ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
54 53 impr 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> A. w e. A ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) )
55 fveq2 
 |-  ( z = m -> ( [,] ` z ) = ( [,] ` m ) )
56 55 sseq1d 
 |-  ( z = m -> ( ( [,] ` z ) C_ ( [,] ` w ) <-> ( [,] ` m ) C_ ( [,] ` w ) ) )
57 equequ1 
 |-  ( z = m -> ( z = w <-> m = w ) )
58 56 57 imbi12d 
 |-  ( z = m -> ( ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
59 58 ralbidv 
 |-  ( z = m -> ( A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> A. w e. A ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
60 59 2 elrab2 
 |-  ( m e. G <-> ( m e. A /\ A. w e. A ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) )
61 38 54 60 sylanbrc 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> m e. G )
62 ffun 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
63 5 62 ax-mp 
 |-  Fun [,]
64 2 ssrab3 
 |-  G C_ A
65 64 15 sstrid 
 |-  ( ph -> G C_ ( RR* X. RR* ) )
66 5 fdmi 
 |-  dom [,] = ( RR* X. RR* )
67 65 66 sseqtrrdi 
 |-  ( ph -> G C_ dom [,] )
68 67 ad2antrr 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> G C_ dom [,] )
69 funfvima2 
 |-  ( ( Fun [,] /\ G C_ dom [,] ) -> ( m e. G -> ( [,] ` m ) e. ( [,] " G ) ) )
70 63 68 69 sylancr 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> ( m e. G -> ( [,] ` m ) e. ( [,] " G ) ) )
71 61 70 mpd 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> ( [,] ` m ) e. ( [,] " G ) )
72 elunii 
 |-  ( ( a e. ( [,] ` m ) /\ ( [,] ` m ) e. ( [,] " G ) ) -> a e. U. ( [,] " G ) )
73 37 71 72 syl2anc 
 |-  ( ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) /\ ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) /\ A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) ) ) -> a e. U. ( [,] " G ) )
74 73 exp32 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> ( ( m e. A /\ ( [,] ` t ) C_ ( [,] ` m ) ) -> ( A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) -> a e. U. ( [,] " G ) ) ) )
75 34 74 syl5bi 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> ( m e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } -> ( A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) -> a e. U. ( [,] " G ) ) ) )
76 75 rexlimdv 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> ( E. m e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } A. w e. { a e. A | ( [,] ` t ) C_ ( [,] ` a ) } ( ( [,] ` m ) C_ ( [,] ` w ) -> m = w ) -> a e. U. ( [,] " G ) ) )
77 31 76 mpd 
 |-  ( ( ph /\ ( t e. A /\ a e. ( [,] ` t ) ) ) -> a e. U. ( [,] " G ) )
78 77 rexlimdvaa 
 |-  ( ph -> ( E. t e. A a e. ( [,] ` t ) -> a e. U. ( [,] " G ) ) )
79 18 78 sylbid 
 |-  ( ph -> ( E. i e. ( [,] " A ) a e. i -> a e. U. ( [,] " G ) ) )
80 4 79 syl5bi 
 |-  ( ph -> ( a e. U. ( [,] " A ) -> a e. U. ( [,] " G ) ) )
81 80 ssrdv 
 |-  ( ph -> U. ( [,] " A ) C_ U. ( [,] " G ) )
82 imass2 
 |-  ( G C_ A -> ( [,] " G ) C_ ( [,] " A ) )
83 64 82 ax-mp 
 |-  ( [,] " G ) C_ ( [,] " A )
84 uniss 
 |-  ( ( [,] " G ) C_ ( [,] " A ) -> U. ( [,] " G ) C_ U. ( [,] " A ) )
85 83 84 mp1i 
 |-  ( ph -> U. ( [,] " G ) C_ U. ( [,] " A ) )
86 81 85 eqssd 
 |-  ( ph -> U. ( [,] " A ) = U. ( [,] " G ) )