Step |
Hyp |
Ref |
Expression |
1 |
|
ivthicc.1 |
|- ( ph -> A e. RR ) |
2 |
|
ivthicc.2 |
|- ( ph -> B e. RR ) |
3 |
|
ivthicc.3 |
|- ( ph -> M e. ( A [,] B ) ) |
4 |
|
ivthicc.4 |
|- ( ph -> N e. ( A [,] B ) ) |
5 |
|
ivthicc.5 |
|- ( ph -> ( A [,] B ) C_ D ) |
6 |
|
ivthicc.7 |
|- ( ph -> F e. ( D -cn-> CC ) ) |
7 |
|
ivthicc.8 |
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR ) |
8 |
|
simpll |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> ph ) |
9 |
|
elicc2 |
|- ( ( A e. RR /\ B e. RR ) -> ( M e. ( A [,] B ) <-> ( M e. RR /\ A <_ M /\ M <_ B ) ) ) |
10 |
1 2 9
|
syl2anc |
|- ( ph -> ( M e. ( A [,] B ) <-> ( M e. RR /\ A <_ M /\ M <_ B ) ) ) |
11 |
3 10
|
mpbid |
|- ( ph -> ( M e. RR /\ A <_ M /\ M <_ B ) ) |
12 |
11
|
simp1d |
|- ( ph -> M e. RR ) |
13 |
12
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> M e. RR ) |
14 |
|
elicc2 |
|- ( ( A e. RR /\ B e. RR ) -> ( N e. ( A [,] B ) <-> ( N e. RR /\ A <_ N /\ N <_ B ) ) ) |
15 |
1 2 14
|
syl2anc |
|- ( ph -> ( N e. ( A [,] B ) <-> ( N e. RR /\ A <_ N /\ N <_ B ) ) ) |
16 |
4 15
|
mpbid |
|- ( ph -> ( N e. RR /\ A <_ N /\ N <_ B ) ) |
17 |
16
|
simp1d |
|- ( ph -> N e. RR ) |
18 |
17
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> N e. RR ) |
19 |
|
fveq2 |
|- ( x = M -> ( F ` x ) = ( F ` M ) ) |
20 |
19
|
eleq1d |
|- ( x = M -> ( ( F ` x ) e. RR <-> ( F ` M ) e. RR ) ) |
21 |
7
|
ralrimiva |
|- ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR ) |
22 |
20 21 3
|
rspcdva |
|- ( ph -> ( F ` M ) e. RR ) |
23 |
|
fveq2 |
|- ( x = N -> ( F ` x ) = ( F ` N ) ) |
24 |
23
|
eleq1d |
|- ( x = N -> ( ( F ` x ) e. RR <-> ( F ` N ) e. RR ) ) |
25 |
24 21 4
|
rspcdva |
|- ( ph -> ( F ` N ) e. RR ) |
26 |
|
iccssre |
|- ( ( ( F ` M ) e. RR /\ ( F ` N ) e. RR ) -> ( ( F ` M ) [,] ( F ` N ) ) C_ RR ) |
27 |
22 25 26
|
syl2anc |
|- ( ph -> ( ( F ` M ) [,] ( F ` N ) ) C_ RR ) |
28 |
27
|
sselda |
|- ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> y e. RR ) |
29 |
28
|
adantr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> y e. RR ) |
30 |
|
simpr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> M < N ) |
31 |
11
|
simp2d |
|- ( ph -> A <_ M ) |
32 |
16
|
simp3d |
|- ( ph -> N <_ B ) |
33 |
|
iccss |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ M /\ N <_ B ) ) -> ( M [,] N ) C_ ( A [,] B ) ) |
34 |
1 2 31 32 33
|
syl22anc |
|- ( ph -> ( M [,] N ) C_ ( A [,] B ) ) |
35 |
34 5
|
sstrd |
|- ( ph -> ( M [,] N ) C_ D ) |
36 |
35
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> ( M [,] N ) C_ D ) |
37 |
6
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> F e. ( D -cn-> CC ) ) |
38 |
34
|
sselda |
|- ( ( ph /\ x e. ( M [,] N ) ) -> x e. ( A [,] B ) ) |
39 |
38 7
|
syldan |
|- ( ( ph /\ x e. ( M [,] N ) ) -> ( F ` x ) e. RR ) |
40 |
8 39
|
sylan |
|- ( ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) /\ x e. ( M [,] N ) ) -> ( F ` x ) e. RR ) |
41 |
|
elicc2 |
|- ( ( ( F ` M ) e. RR /\ ( F ` N ) e. RR ) -> ( y e. ( ( F ` M ) [,] ( F ` N ) ) <-> ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) ) |
42 |
22 25 41
|
syl2anc |
|- ( ph -> ( y e. ( ( F ` M ) [,] ( F ` N ) ) <-> ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) ) |
43 |
42
|
biimpa |
|- ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) |
44 |
|
3simpc |
|- ( ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) |
45 |
43 44
|
syl |
|- ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) |
46 |
45
|
adantr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) |
47 |
13 18 29 30 36 37 40 46
|
ivthle |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> E. z e. ( M [,] N ) ( F ` z ) = y ) |
48 |
35
|
sselda |
|- ( ( ph /\ z e. ( M [,] N ) ) -> z e. D ) |
49 |
|
cncff |
|- ( F e. ( D -cn-> CC ) -> F : D --> CC ) |
50 |
|
ffn |
|- ( F : D --> CC -> F Fn D ) |
51 |
6 49 50
|
3syl |
|- ( ph -> F Fn D ) |
52 |
|
fnfvelrn |
|- ( ( F Fn D /\ z e. D ) -> ( F ` z ) e. ran F ) |
53 |
51 52
|
sylan |
|- ( ( ph /\ z e. D ) -> ( F ` z ) e. ran F ) |
54 |
|
eleq1 |
|- ( ( F ` z ) = y -> ( ( F ` z ) e. ran F <-> y e. ran F ) ) |
55 |
53 54
|
syl5ibcom |
|- ( ( ph /\ z e. D ) -> ( ( F ` z ) = y -> y e. ran F ) ) |
56 |
48 55
|
syldan |
|- ( ( ph /\ z e. ( M [,] N ) ) -> ( ( F ` z ) = y -> y e. ran F ) ) |
57 |
56
|
rexlimdva |
|- ( ph -> ( E. z e. ( M [,] N ) ( F ` z ) = y -> y e. ran F ) ) |
58 |
8 47 57
|
sylc |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> y e. ran F ) |
59 |
|
simplr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y e. ( ( F ` M ) [,] ( F ` N ) ) ) |
60 |
|
simpr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> M = N ) |
61 |
60
|
fveq2d |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( F ` M ) = ( F ` N ) ) |
62 |
61
|
oveq2d |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( ( F ` M ) [,] ( F ` M ) ) = ( ( F ` M ) [,] ( F ` N ) ) ) |
63 |
22
|
rexrd |
|- ( ph -> ( F ` M ) e. RR* ) |
64 |
63
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( F ` M ) e. RR* ) |
65 |
|
iccid |
|- ( ( F ` M ) e. RR* -> ( ( F ` M ) [,] ( F ` M ) ) = { ( F ` M ) } ) |
66 |
64 65
|
syl |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( ( F ` M ) [,] ( F ` M ) ) = { ( F ` M ) } ) |
67 |
62 66
|
eqtr3d |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( ( F ` M ) [,] ( F ` N ) ) = { ( F ` M ) } ) |
68 |
59 67
|
eleqtrd |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y e. { ( F ` M ) } ) |
69 |
|
elsni |
|- ( y e. { ( F ` M ) } -> y = ( F ` M ) ) |
70 |
68 69
|
syl |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y = ( F ` M ) ) |
71 |
5 3
|
sseldd |
|- ( ph -> M e. D ) |
72 |
|
fnfvelrn |
|- ( ( F Fn D /\ M e. D ) -> ( F ` M ) e. ran F ) |
73 |
51 71 72
|
syl2anc |
|- ( ph -> ( F ` M ) e. ran F ) |
74 |
73
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( F ` M ) e. ran F ) |
75 |
70 74
|
eqeltrd |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y e. ran F ) |
76 |
|
simpll |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> ph ) |
77 |
17
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> N e. RR ) |
78 |
12
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> M e. RR ) |
79 |
28
|
adantr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> y e. RR ) |
80 |
|
simpr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> N < M ) |
81 |
16
|
simp2d |
|- ( ph -> A <_ N ) |
82 |
11
|
simp3d |
|- ( ph -> M <_ B ) |
83 |
|
iccss |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ N /\ M <_ B ) ) -> ( N [,] M ) C_ ( A [,] B ) ) |
84 |
1 2 81 82 83
|
syl22anc |
|- ( ph -> ( N [,] M ) C_ ( A [,] B ) ) |
85 |
84 5
|
sstrd |
|- ( ph -> ( N [,] M ) C_ D ) |
86 |
85
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> ( N [,] M ) C_ D ) |
87 |
6
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> F e. ( D -cn-> CC ) ) |
88 |
84
|
sselda |
|- ( ( ph /\ x e. ( N [,] M ) ) -> x e. ( A [,] B ) ) |
89 |
88 7
|
syldan |
|- ( ( ph /\ x e. ( N [,] M ) ) -> ( F ` x ) e. RR ) |
90 |
76 89
|
sylan |
|- ( ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) /\ x e. ( N [,] M ) ) -> ( F ` x ) e. RR ) |
91 |
45
|
adantr |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) |
92 |
77 78 79 80 86 87 90 91
|
ivthle2 |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> E. z e. ( N [,] M ) ( F ` z ) = y ) |
93 |
85
|
sselda |
|- ( ( ph /\ z e. ( N [,] M ) ) -> z e. D ) |
94 |
93 55
|
syldan |
|- ( ( ph /\ z e. ( N [,] M ) ) -> ( ( F ` z ) = y -> y e. ran F ) ) |
95 |
94
|
rexlimdva |
|- ( ph -> ( E. z e. ( N [,] M ) ( F ` z ) = y -> y e. ran F ) ) |
96 |
76 92 95
|
sylc |
|- ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> y e. ran F ) |
97 |
12 17
|
lttri4d |
|- ( ph -> ( M < N \/ M = N \/ N < M ) ) |
98 |
97
|
adantr |
|- ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> ( M < N \/ M = N \/ N < M ) ) |
99 |
58 75 96 98
|
mpjao3dan |
|- ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> y e. ran F ) |
100 |
99
|
ex |
|- ( ph -> ( y e. ( ( F ` M ) [,] ( F ` N ) ) -> y e. ran F ) ) |
101 |
100
|
ssrdv |
|- ( ph -> ( ( F ` M ) [,] ( F ` N ) ) C_ ran F ) |