Step |
Hyp |
Ref |
Expression |
1 |
|
dyadmbl.1 |
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) |
2 |
1
|
dyadf |
|- F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) |
3 |
|
ffn |
|- ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> F Fn ( ZZ X. NN0 ) ) |
4 |
|
ovelrn |
|- ( F Fn ( ZZ X. NN0 ) -> ( A e. ran F <-> E. a e. ZZ E. c e. NN0 A = ( a F c ) ) ) |
5 |
|
ovelrn |
|- ( F Fn ( ZZ X. NN0 ) -> ( B e. ran F <-> E. b e. ZZ E. d e. NN0 B = ( b F d ) ) ) |
6 |
4 5
|
anbi12d |
|- ( F Fn ( ZZ X. NN0 ) -> ( ( A e. ran F /\ B e. ran F ) <-> ( E. a e. ZZ E. c e. NN0 A = ( a F c ) /\ E. b e. ZZ E. d e. NN0 B = ( b F d ) ) ) ) |
7 |
2 3 6
|
mp2b |
|- ( ( A e. ran F /\ B e. ran F ) <-> ( E. a e. ZZ E. c e. NN0 A = ( a F c ) /\ E. b e. ZZ E. d e. NN0 B = ( b F d ) ) ) |
8 |
|
reeanv |
|- ( E. a e. ZZ E. b e. ZZ ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) <-> ( E. a e. ZZ E. c e. NN0 A = ( a F c ) /\ E. b e. ZZ E. d e. NN0 B = ( b F d ) ) ) |
9 |
7 8
|
bitr4i |
|- ( ( A e. ran F /\ B e. ran F ) <-> E. a e. ZZ E. b e. ZZ ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) ) |
10 |
|
reeanv |
|- ( E. c e. NN0 E. d e. NN0 ( A = ( a F c ) /\ B = ( b F d ) ) <-> ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) ) |
11 |
|
nn0re |
|- ( c e. NN0 -> c e. RR ) |
12 |
11
|
ad2antrl |
|- ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> c e. RR ) |
13 |
|
nn0re |
|- ( d e. NN0 -> d e. RR ) |
14 |
13
|
ad2antll |
|- ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> d e. RR ) |
15 |
1
|
dyaddisjlem |
|- ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) /\ c <_ d ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
16 |
|
ancom |
|- ( ( a e. ZZ /\ b e. ZZ ) <-> ( b e. ZZ /\ a e. ZZ ) ) |
17 |
|
ancom |
|- ( ( c e. NN0 /\ d e. NN0 ) <-> ( d e. NN0 /\ c e. NN0 ) ) |
18 |
16 17
|
anbi12i |
|- ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) <-> ( ( b e. ZZ /\ a e. ZZ ) /\ ( d e. NN0 /\ c e. NN0 ) ) ) |
19 |
1
|
dyaddisjlem |
|- ( ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( d e. NN0 /\ c e. NN0 ) ) /\ d <_ c ) -> ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) ) |
20 |
18 19
|
sylanb |
|- ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) /\ d <_ c ) -> ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) ) |
21 |
|
orcom |
|- ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) ) |
22 |
|
incom |
|- ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) |
23 |
22
|
eqeq1i |
|- ( ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) <-> ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) |
24 |
21 23
|
orbi12i |
|- ( ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) <-> ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
25 |
|
df-3or |
|- ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) <-> ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) ) |
26 |
|
df-3or |
|- ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) <-> ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
27 |
24 25 26
|
3bitr4i |
|- ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
28 |
20 27
|
sylib |
|- ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) /\ d <_ c ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
29 |
12 14 15 28
|
lecasei |
|- ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
30 |
|
simpl |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> A = ( a F c ) ) |
31 |
30
|
fveq2d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( [,] ` A ) = ( [,] ` ( a F c ) ) ) |
32 |
|
simpr |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> B = ( b F d ) ) |
33 |
32
|
fveq2d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( [,] ` B ) = ( [,] ` ( b F d ) ) ) |
34 |
31 33
|
sseq12d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) <-> ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) |
35 |
33 31
|
sseq12d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` B ) C_ ( [,] ` A ) <-> ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) ) |
36 |
30
|
fveq2d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( (,) ` A ) = ( (,) ` ( a F c ) ) ) |
37 |
32
|
fveq2d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( (,) ` B ) = ( (,) ` ( b F d ) ) ) |
38 |
36 37
|
ineq12d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( (,) ` A ) i^i ( (,) ` B ) ) = ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) ) |
39 |
38
|
eqeq1d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) <-> ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) |
40 |
34 35 39
|
3orbi123d |
|- ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) ) |
41 |
29 40
|
syl5ibrcom |
|- ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) ) |
42 |
41
|
rexlimdvva |
|- ( ( a e. ZZ /\ b e. ZZ ) -> ( E. c e. NN0 E. d e. NN0 ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) ) |
43 |
10 42
|
syl5bir |
|- ( ( a e. ZZ /\ b e. ZZ ) -> ( ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) ) |
44 |
43
|
rexlimivv |
|- ( E. a e. ZZ E. b e. ZZ ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) |
45 |
9 44
|
sylbi |
|- ( ( A e. ran F /\ B e. ran F ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) |