Step | Hyp | Ref
| Expression |
1 | | ordtNEW.l |
. . . . 5
|
2 | | fvex 6201 |
. . . . . 6
|
3 | 2 | inex1 4799 |
. . . . 5
|
4 | 1, 3 | eqeltri 2697 |
. . . 4
|
5 | 4 | inex1 4799 |
. . 3
|
6 | | eqid 2622 |
. . . 4
|
7 | | eqid 2622 |
. . . 4
|
8 | | eqid 2622 |
. . . 4
|
9 | 6, 7, 8 | ordtval 20993 |
. . 3
ordTop |
10 | 5, 9 | mp1i 13 |
. 2
ordTop
|
11 | | ordttop 21004 |
. . . . . 6
ordTop |
12 | 4, 11 | ax-mp 5 |
. . . . 5
ordTop |
13 | | ordtNEW.b |
. . . . . . 7
|
14 | | fvex 6201 |
. . . . . . 7
|
15 | 13, 14 | eqeltri 2697 |
. . . . . 6
|
16 | 15 | ssex 4802 |
. . . . 5
|
17 | | resttop 20964 |
. . . . 5
ordTop
ordTop
↾t |
18 | 12, 16, 17 | sylancr 695 |
. . . 4
ordTop ↾t |
19 | 18 | adantl 482 |
. . 3
ordTop ↾t |
20 | 13 | ressprs 29655 |
. . . . . . . . 9
↾s |
21 | | eqid 2622 |
. . . . . . . . . 10
↾s ↾s |
22 | | eqid 2622 |
. . . . . . . . . 10
↾s ↾s ↾s
↾s ↾s ↾s |
23 | 21, 22 | prsdm 29960 |
. . . . . . . . 9
↾s
↾s ↾s ↾s
↾s |
24 | 20, 23 | syl 17 |
. . . . . . . 8
↾s ↾s ↾s
↾s |
25 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾s ↾s |
26 | 25, 13 | ressbas2 15931 |
. . . . . . . . . . . . 13
↾s |
27 | | fvex 6201 |
. . . . . . . . . . . . 13
↾s |
28 | 26, 27 | syl6eqel 2709 |
. . . . . . . . . . . 12
|
29 | | eqid 2622 |
. . . . . . . . . . . . 13
|
30 | 25, 29 | ressle 16059 |
. . . . . . . . . . . 12
↾s |
31 | 28, 30 | syl 17 |
. . . . . . . . . . 11
↾s |
32 | 31 | adantl 482 |
. . . . . . . . . 10
↾s |
33 | 26 | adantl 482 |
. . . . . . . . . . 11
↾s |
34 | 33 | sqxpeqd 5141 |
. . . . . . . . . 10
↾s ↾s |
35 | 32, 34 | ineq12d 3815 |
. . . . . . . . 9
↾s ↾s ↾s |
36 | 35 | dmeqd 5326 |
. . . . . . . 8
↾s ↾s ↾s |
37 | 24, 36, 33 | 3eqtr4d 2666 |
. . . . . . 7
|
38 | 13, 1 | prsss 29962 |
. . . . . . . 8
|
39 | 38 | dmeqd 5326 |
. . . . . . 7
|
40 | 13, 1 | prsdm 29960 |
. . . . . . . . . 10
|
41 | 40 | sseq2d 3633 |
. . . . . . . . 9
|
42 | 41 | biimpar 502 |
. . . . . . . 8
|
43 | | sseqin2 3817 |
. . . . . . . 8
|
44 | 42, 43 | sylib 208 |
. . . . . . 7
|
45 | 37, 39, 44 | 3eqtr4d 2666 |
. . . . . 6
|
46 | 4, 11 | mp1i 13 |
. . . . . . 7
ordTop
|
47 | 16 | adantl 482 |
. . . . . . 7
|
48 | | eqid 2622 |
. . . . . . . . . 10
|
49 | 48 | ordttopon 20997 |
. . . . . . . . 9
ordTop TopOn |
50 | 4, 49 | mp1i 13 |
. . . . . . . 8
ordTop
TopOn |
51 | | toponmax 20730 |
. . . . . . . 8
ordTop TopOn ordTop
|
52 | 50, 51 | syl 17 |
. . . . . . 7
ordTop
|
53 | | elrestr 16089 |
. . . . . . 7
ordTop
ordTop
ordTop
↾t |
54 | 46, 47, 52, 53 | syl3anc 1326 |
. . . . . 6
ordTop ↾t |
55 | 45, 54 | eqeltrd 2701 |
. . . . 5
ordTop ↾t |
56 | 55 | snssd 4340 |
. . . 4
ordTop ↾t |
57 | | rabeq 3192 |
. . . . . . . . 9
|
58 | 45, 57 | syl 17 |
. . . . . . . 8
|
59 | 45, 58 | mpteq12dv 4733 |
. . . . . . 7
|
60 | 59 | rneqd 5353 |
. . . . . 6
|
61 | | inrab2 3900 |
. . . . . . . . . 10
|
62 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
63 | | simpr 477 |
. . . . . . . . . . . . . 14
|
64 | 62, 63 | sseldi 3601 |
. . . . . . . . . . . . 13
|
65 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
66 | 62, 65 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
67 | 66 | adantr 481 |
. . . . . . . . . . . . 13
|
68 | | brinxp 5181 |
. . . . . . . . . . . . 13
|
69 | 64, 67, 68 | syl2anc 693 |
. . . . . . . . . . . 12
|
70 | 69 | notbid 308 |
. . . . . . . . . . 11
|
71 | 70 | rabbidva 3188 |
. . . . . . . . . 10
|
72 | 61, 71 | syl5eq 2668 |
. . . . . . . . 9
|
73 | 4, 11 | mp1i 13 |
. . . . . . . . . 10
ordTop |
74 | 47 | adantr 481 |
. . . . . . . . . 10
|
75 | | simpl 473 |
. . . . . . . . . . 11
|
76 | | inss1 3833 |
. . . . . . . . . . . 12
|
77 | 76 | sseli 3599 |
. . . . . . . . . . 11
|
78 | 48 | ordtopn1 20998 |
. . . . . . . . . . . . 13
ordTop |
79 | 4, 78 | mpan 706 |
. . . . . . . . . . . 12
ordTop |
80 | 79 | adantl 482 |
. . . . . . . . . . 11
ordTop |
81 | 75, 77, 80 | syl2an 494 |
. . . . . . . . . 10
ordTop |
82 | | elrestr 16089 |
. . . . . . . . . 10
ordTop
ordTop ordTop
↾t |
83 | 73, 74, 81, 82 | syl3anc 1326 |
. . . . . . . . 9
ordTop
↾t |
84 | 72, 83 | eqeltrrd 2702 |
. . . . . . . 8
ordTop
↾t |
85 | | eqid 2622 |
. . . . . . . 8
|
86 | 84, 85 | fmptd 6385 |
. . . . . . 7
ordTop
↾t |
87 | | frn 6053 |
. . . . . . 7
ordTop
↾t
ordTop ↾t |
88 | 86, 87 | syl 17 |
. . . . . 6
ordTop
↾t |
89 | 60, 88 | eqsstrd 3639 |
. . . . 5
ordTop
↾t |
90 | | rabeq 3192 |
. . . . . . . . 9
|
91 | 45, 90 | syl 17 |
. . . . . . . 8
|
92 | 45, 91 | mpteq12dv 4733 |
. . . . . . 7
|
93 | 92 | rneqd 5353 |
. . . . . 6
|
94 | | inrab2 3900 |
. . . . . . . . . 10
|
95 | | brinxp 5181 |
. . . . . . . . . . . . 13
|
96 | 67, 64, 95 | syl2anc 693 |
. . . . . . . . . . . 12
|
97 | 96 | notbid 308 |
. . . . . . . . . . 11
|
98 | 97 | rabbidva 3188 |
. . . . . . . . . 10
|
99 | 94, 98 | syl5eq 2668 |
. . . . . . . . 9
|
100 | 48 | ordtopn2 20999 |
. . . . . . . . . . . . 13
ordTop |
101 | 4, 100 | mpan 706 |
. . . . . . . . . . . 12
ordTop |
102 | 101 | adantl 482 |
. . . . . . . . . . 11
ordTop |
103 | 75, 77, 102 | syl2an 494 |
. . . . . . . . . 10
ordTop |
104 | | elrestr 16089 |
. . . . . . . . . 10
ordTop
ordTop ordTop
↾t |
105 | 73, 74, 103, 104 | syl3anc 1326 |
. . . . . . . . 9
ordTop ↾t |
106 | 99, 105 | eqeltrrd 2702 |
. . . . . . . 8
ordTop
↾t |
107 | | eqid 2622 |
. . . . . . . 8
|
108 | 106, 107 | fmptd 6385 |
. . . . . . 7
ordTop
↾t |
109 | | frn 6053 |
. . . . . . 7
ordTop
↾t
ordTop ↾t |
110 | 108, 109 | syl 17 |
. . . . . 6
ordTop
↾t |
111 | 93, 110 | eqsstrd 3639 |
. . . . 5
ordTop
↾t |
112 | 89, 111 | unssd 3789 |
. . . 4
ordTop ↾t |
113 | 56, 112 | unssd 3789 |
. . 3
ordTop
↾t |
114 | | tgfiss 20795 |
. . 3
ordTop ↾t
ordTop
↾t
ordTop
↾t |
115 | 19, 113, 114 | syl2anc 693 |
. 2
ordTop
↾t |
116 | 10, 115 | eqsstrd 3639 |
1
ordTop
ordTop
↾t |