Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . 6
↾t |
2 | | elfi2 8320 |
. . . . . 6
↾t ↾t
↾t |
3 | 1, 2 | ax-mp 5 |
. . . . 5
↾t
↾t |
4 | | eldifi 3732 |
. . . . . . . . . . 11
↾t ↾t |
5 | 4 | adantl 482 |
. . . . . . . . . 10
↾t ↾t |
6 | | elfpw 8268 |
. . . . . . . . . . 11
↾t ↾t |
7 | 6 | simprbi 480 |
. . . . . . . . . 10
↾t |
8 | 5, 7 | syl 17 |
. . . . . . . . 9
↾t |
9 | 6 | simplbi 476 |
. . . . . . . . . . . . 13
↾t ↾t |
10 | 5, 9 | syl 17 |
. . . . . . . . . . . 12
↾t ↾t |
11 | 10 | sseld 3602 |
. . . . . . . . . . 11
↾t
↾t |
12 | | elrest 16088 |
. . . . . . . . . . . 12
↾t
|
13 | 12 | adantr 481 |
. . . . . . . . . . 11
↾t
↾t
|
14 | 11, 13 | sylibd 229 |
. . . . . . . . . 10
↾t
|
15 | 14 | ralrimiv 2965 |
. . . . . . . . 9
↾t
|
16 | | ineq1 3807 |
. . . . . . . . . . 11
|
17 | 16 | eqeq2d 2632 |
. . . . . . . . . 10
|
18 | 17 | ac6sfi 8204 |
. . . . . . . . 9
|
19 | 8, 15, 18 | syl2anc 693 |
. . . . . . . 8
↾t |
20 | | eldifsni 4320 |
. . . . . . . . . . . . . 14
↾t |
21 | 20 | ad2antlr 763 |
. . . . . . . . . . . . 13
↾t |
22 | | iinin1 4591 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
↾t
|
24 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
↾t |
26 | | simpllr 799 |
. . . . . . . . . . . . 13
↾t
|
27 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . 15
↾t |
29 | | fniinfv 6257 |
. . . . . . . . . . . . . . 15
|
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . 14
↾t |
31 | | simplll 798 |
. . . . . . . . . . . . . . 15
↾t
|
32 | | simpr 477 |
. . . . . . . . . . . . . . 15
↾t |
33 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
↾t |
34 | | intrnfi 8322 |
. . . . . . . . . . . . . . 15
|
35 | 31, 32, 21, 33, 34 | syl13anc 1328 |
. . . . . . . . . . . . . 14
↾t |
36 | 30, 35 | eqeltrd 2701 |
. . . . . . . . . . . . 13
↾t |
37 | | elrestr 16089 |
. . . . . . . . . . . . 13
↾t |
38 | 25, 26, 36, 37 | syl3anc 1326 |
. . . . . . . . . . . 12
↾t
↾t |
39 | 23, 38 | eqeltrd 2701 |
. . . . . . . . . . 11
↾t
↾t |
40 | | intiin 4574 |
. . . . . . . . . . . . 13
|
41 | | iineq2 4538 |
. . . . . . . . . . . . 13
|
42 | 40, 41 | syl5eq 2668 |
. . . . . . . . . . . 12
|
43 | 42 | eleq1d 2686 |
. . . . . . . . . . 11
↾t
↾t |
44 | 39, 43 | syl5ibrcom 237 |
. . . . . . . . . 10
↾t
↾t |
45 | 44 | expimpd 629 |
. . . . . . . . 9
↾t
↾t |
46 | 45 | exlimdv 1861 |
. . . . . . . 8
↾t
↾t |
47 | 19, 46 | mpd 15 |
. . . . . . 7
↾t ↾t |
48 | | eleq1 2689 |
. . . . . . 7
↾t
↾t |
49 | 47, 48 | syl5ibrcom 237 |
. . . . . 6
↾t
↾t |
50 | 49 | rexlimdva 3031 |
. . . . 5
↾t ↾t |
51 | 3, 50 | syl5bi 232 |
. . . 4
↾t
↾t |
52 | | simpr 477 |
. . . . . 6
|
53 | | elrest 16088 |
. . . . . 6
↾t
|
54 | 24, 52, 53 | sylancr 695 |
. . . . 5
↾t
|
55 | | elfi2 8320 |
. . . . . . . 8
|
56 | 55 | adantr 481 |
. . . . . . 7
|
57 | | eldifsni 4320 |
. . . . . . . . . . . . . 14
|
58 | 57 | adantl 482 |
. . . . . . . . . . . . 13
|
59 | | iinin1 4591 |
. . . . . . . . . . . . 13
|
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
|
61 | 40 | ineq1i 3810 |
. . . . . . . . . . . 12
|
62 | 60, 61 | syl6eqr 2674 |
. . . . . . . . . . 11
|
63 | 1 | a1i 11 |
. . . . . . . . . . . 12
↾t |
64 | | eldifi 3732 |
. . . . . . . . . . . . . . 15
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . . 14
|
66 | | elfpw 8268 |
. . . . . . . . . . . . . . 15
|
67 | 66 | simplbi 476 |
. . . . . . . . . . . . . 14
|
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . 13
|
69 | | elrestr 16089 |
. . . . . . . . . . . . . . . 16
↾t |
70 | 69 | 3expa 1265 |
. . . . . . . . . . . . . . 15
↾t |
71 | 70 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
↾t |
72 | 71 | adantr 481 |
. . . . . . . . . . . . 13
↾t |
73 | | ssralv 3666 |
. . . . . . . . . . . . 13
↾t
↾t |
74 | 68, 72, 73 | sylc 65 |
. . . . . . . . . . . 12
↾t |
75 | 66 | simprbi 480 |
. . . . . . . . . . . . 13
|
76 | 65, 75 | syl 17 |
. . . . . . . . . . . 12
|
77 | | iinfi 8323 |
. . . . . . . . . . . 12
↾t ↾t
↾t |
78 | 63, 74, 58, 76, 77 | syl13anc 1328 |
. . . . . . . . . . 11
↾t |
79 | 62, 78 | eqeltrrd 2702 |
. . . . . . . . . 10
↾t |
80 | | eleq1 2689 |
. . . . . . . . . 10
↾t ↾t |
81 | 79, 80 | syl5ibrcom 237 |
. . . . . . . . 9
↾t |
82 | | ineq1 3807 |
. . . . . . . . . . 11
|
83 | 82 | eqeq2d 2632 |
. . . . . . . . . 10
|
84 | 83 | imbi1d 331 |
. . . . . . . . 9
↾t
↾t |
85 | 81, 84 | syl5ibrcom 237 |
. . . . . . . 8
↾t |
86 | 85 | rexlimdva 3031 |
. . . . . . 7
↾t |
87 | 56, 86 | sylbid 230 |
. . . . . 6
↾t |
88 | 87 | rexlimdv 3030 |
. . . . 5
↾t |
89 | 54, 88 | sylbid 230 |
. . . 4
↾t ↾t |
90 | 51, 89 | impbid 202 |
. . 3
↾t
↾t |
91 | 90 | eqrdv 2620 |
. 2
↾t
↾t |
92 | | fi0 8326 |
. . 3
|
93 | | relxp 5227 |
. . . . . 6
|
94 | | restfn 16085 |
. . . . . . . 8
↾t
|
95 | | fndm 5990 |
. . . . . . . 8
↾t ↾t |
96 | 94, 95 | ax-mp 5 |
. . . . . . 7
↾t
|
97 | 96 | releqi 5202 |
. . . . . 6
↾t |
98 | 93, 97 | mpbir 221 |
. . . . 5
↾t |
99 | 98 | ovprc 6683 |
. . . 4
↾t |
100 | 99 | fveq2d 6195 |
. . 3
↾t |
101 | | ianor 509 |
. . . 4
|
102 | | fvprc 6185 |
. . . . . . 7
|
103 | 102 | oveq1d 6665 |
. . . . . 6
↾t ↾t |
104 | | 0rest 16090 |
. . . . . 6
↾t |
105 | 103, 104 | syl6eq 2672 |
. . . . 5
↾t |
106 | 98 | ovprc2 6685 |
. . . . 5
↾t |
107 | 105, 106 | jaoi 394 |
. . . 4
↾t |
108 | 101, 107 | sylbi 207 |
. . 3
↾t |
109 | 92, 100, 108 | 3eqtr4a 2682 |
. 2
↾t
↾t |
110 | 91, 109 | pm2.61i 176 |
1
↾t ↾t |