Step | Hyp | Ref
| Expression |
1 | | inex1g 4801 |
. . . 4
|
2 | 1 | adantr 481 |
. . 3
|
3 | | eqid 2622 |
. . . 4
|
4 | | eqid 2622 |
. . . 4
|
5 | | eqid 2622 |
. . . 4
|
6 | 3, 4, 5 | ordtval 20993 |
. . 3
ordTop
|
7 | 2, 6 | syl 17 |
. 2
ordTop
|
8 | | ordttop 21004 |
. . . 4
ordTop |
9 | | resttop 20964 |
. . . 4
ordTop ordTop ↾t |
10 | 8, 9 | sylan 488 |
. . 3
ordTop ↾t |
11 | | eqid 2622 |
. . . . . . . 8
|
12 | 11 | psssdm2 17215 |
. . . . . . 7
|
13 | 12 | adantr 481 |
. . . . . 6
|
14 | 8 | adantr 481 |
. . . . . . 7
ordTop |
15 | | simpr 477 |
. . . . . . 7
|
16 | 11 | ordttopon 20997 |
. . . . . . . . 9
ordTop TopOn |
17 | 16 | adantr 481 |
. . . . . . . 8
ordTop TopOn |
18 | | toponmax 20730 |
. . . . . . . 8
ordTop TopOn ordTop |
19 | 17, 18 | syl 17 |
. . . . . . 7
ordTop |
20 | | elrestr 16089 |
. . . . . . 7
ordTop ordTop
ordTop ↾t |
21 | 14, 15, 19, 20 | syl3anc 1326 |
. . . . . 6
ordTop
↾t |
22 | 13, 21 | eqeltrd 2701 |
. . . . 5
ordTop
↾t |
23 | 22 | snssd 4340 |
. . . 4
ordTop
↾t |
24 | | rabeq 3192 |
. . . . . . . . 9
|
25 | 13, 24 | syl 17 |
. . . . . . . 8
|
26 | 13, 25 | mpteq12dv 4733 |
. . . . . . 7
|
27 | 26 | rneqd 5353 |
. . . . . 6
|
28 | | inrab2 3900 |
. . . . . . . . . 10
|
29 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
30 | | simpr 477 |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | sseldi 3601 |
. . . . . . . . . . . . 13
|
32 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
33 | 29, 32 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
|
35 | | brinxp 5181 |
. . . . . . . . . . . . 13
|
36 | 31, 34, 35 | syl2anc 693 |
. . . . . . . . . . . 12
|
37 | 36 | notbid 308 |
. . . . . . . . . . 11
|
38 | 37 | rabbidva 3188 |
. . . . . . . . . 10
|
39 | 28, 38 | syl5eq 2668 |
. . . . . . . . 9
|
40 | 14 | adantr 481 |
. . . . . . . . . 10
ordTop |
41 | 15 | adantr 481 |
. . . . . . . . . 10
|
42 | | simpl 473 |
. . . . . . . . . . 11
|
43 | | inss1 3833 |
. . . . . . . . . . . 12
|
44 | 43 | sseli 3599 |
. . . . . . . . . . 11
|
45 | 11 | ordtopn1 20998 |
. . . . . . . . . . 11
ordTop |
46 | 42, 44, 45 | syl2an 494 |
. . . . . . . . . 10
ordTop |
47 | | elrestr 16089 |
. . . . . . . . . 10
ordTop ordTop
ordTop
↾t |
48 | 40, 41, 46, 47 | syl3anc 1326 |
. . . . . . . . 9
ordTop
↾t |
49 | 39, 48 | eqeltrrd 2702 |
. . . . . . . 8
ordTop ↾t |
50 | | eqid 2622 |
. . . . . . . 8
|
51 | 49, 50 | fmptd 6385 |
. . . . . . 7
ordTop
↾t |
52 | | frn 6053 |
. . . . . . 7
ordTop
↾t
ordTop ↾t |
53 | 51, 52 | syl 17 |
. . . . . 6
ordTop ↾t |
54 | 27, 53 | eqsstrd 3639 |
. . . . 5
ordTop ↾t |
55 | | rabeq 3192 |
. . . . . . . . 9
|
56 | 13, 55 | syl 17 |
. . . . . . . 8
|
57 | 13, 56 | mpteq12dv 4733 |
. . . . . . 7
|
58 | 57 | rneqd 5353 |
. . . . . 6
|
59 | | inrab2 3900 |
. . . . . . . . . 10
|
60 | | brinxp 5181 |
. . . . . . . . . . . . 13
|
61 | 34, 31, 60 | syl2anc 693 |
. . . . . . . . . . . 12
|
62 | 61 | notbid 308 |
. . . . . . . . . . 11
|
63 | 62 | rabbidva 3188 |
. . . . . . . . . 10
|
64 | 59, 63 | syl5eq 2668 |
. . . . . . . . 9
|
65 | 11 | ordtopn2 20999 |
. . . . . . . . . . 11
ordTop |
66 | 42, 44, 65 | syl2an 494 |
. . . . . . . . . 10
ordTop |
67 | | elrestr 16089 |
. . . . . . . . . 10
ordTop ordTop ordTop
↾t |
68 | 40, 41, 66, 67 | syl3anc 1326 |
. . . . . . . . 9
ordTop
↾t |
69 | 64, 68 | eqeltrrd 2702 |
. . . . . . . 8
ordTop ↾t |
70 | | eqid 2622 |
. . . . . . . 8
|
71 | 69, 70 | fmptd 6385 |
. . . . . . 7
ordTop
↾t |
72 | | frn 6053 |
. . . . . . 7
ordTop
↾t
ordTop ↾t |
73 | 71, 72 | syl 17 |
. . . . . 6
ordTop ↾t |
74 | 58, 73 | eqsstrd 3639 |
. . . . 5
ordTop ↾t |
75 | 54, 74 | unssd 3789 |
. . . 4
ordTop ↾t |
76 | 23, 75 | unssd 3789 |
. . 3
ordTop
↾t |
77 | | tgfiss 20795 |
. . 3
ordTop ↾t
ordTop
↾t
ordTop ↾t |
78 | 10, 76, 77 | syl2anc 693 |
. 2
ordTop ↾t |
79 | 7, 78 | eqsstrd 3639 |
1
ordTop
ordTop
↾t |