Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
|
2 | | eqid 2622 |
. . . 4
|
3 | 1, 2 | leordtval2 21016 |
. . 3
ordTop |
4 | | fvex 6201 |
. . . 4
|
5 | | fvex 6201 |
. . . . . 6
ordTop |
6 | | lecldbas.1 |
. . . . . . . 8
|
7 | | iccf 12272 |
. . . . . . . . . . 11
|
8 | | ffn 6045 |
. . . . . . . . . . 11
|
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
|
10 | | ovelrn 6810 |
. . . . . . . . . 10
|
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
|
12 | | difeq2 3722 |
. . . . . . . . . . . 12
|
13 | | iccordt 21018 |
. . . . . . . . . . . . 13
ordTop |
14 | | letopuni 21011 |
. . . . . . . . . . . . . 14
ordTop
|
15 | 14 | cldopn 20835 |
. . . . . . . . . . . . 13
ordTop ordTop
|
16 | 13, 15 | ax-mp 5 |
. . . . . . . . . . . 12
ordTop |
17 | 12, 16 | syl6eqel 2709 |
. . . . . . . . . . 11
ordTop
|
18 | 17 | rexlimivw 3029 |
. . . . . . . . . 10
ordTop
|
19 | 18 | rexlimivw 3029 |
. . . . . . . . 9
ordTop |
20 | 11, 19 | sylbi 207 |
. . . . . . . 8
ordTop
|
21 | 6, 20 | fmpti 6383 |
. . . . . . 7
ordTop
|
22 | | frn 6053 |
. . . . . . 7
ordTop
ordTop
|
23 | 21, 22 | ax-mp 5 |
. . . . . 6
ordTop
|
24 | 5, 23 | ssexi 4803 |
. . . . 5
|
25 | | eqid 2622 |
. . . . . . . 8
|
26 | | mnfxr 10096 |
. . . . . . . . . . 11
|
27 | | fnovrn 6809 |
. . . . . . . . . . 11
|
28 | 9, 26, 27 | mp3an12 1414 |
. . . . . . . . . 10
|
29 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
|
30 | | id 22 |
. . . . . . . . . . . . . 14
|
31 | | pnfxr 10092 |
. . . . . . . . . . . . . . 15
|
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
|
33 | | mnfle 11969 |
. . . . . . . . . . . . . 14
|
34 | | pnfge 11964 |
. . . . . . . . . . . . . 14
|
35 | | df-icc 12182 |
. . . . . . . . . . . . . . 15
|
36 | | df-ioc 12180 |
. . . . . . . . . . . . . . 15
|
37 | | xrltnle 10105 |
. . . . . . . . . . . . . . 15
|
38 | | xrletr 11989 |
. . . . . . . . . . . . . . 15
|
39 | | xrlelttr 11987 |
. . . . . . . . . . . . . . . 16
|
40 | | xrltle 11982 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
|
42 | 39, 41 | syld 47 |
. . . . . . . . . . . . . . 15
|
43 | 35, 36, 37, 35, 38, 42 | ixxun 12191 |
. . . . . . . . . . . . . 14
|
44 | 29, 30, 32, 33, 34, 43 | syl32anc 1334 |
. . . . . . . . . . . . 13
|
45 | | iccmax 12249 |
. . . . . . . . . . . . 13
|
46 | 44, 45 | syl6eq 2672 |
. . . . . . . . . . . 12
|
47 | | iccssxr 12256 |
. . . . . . . . . . . . 13
|
48 | 35, 36, 37 | ixxdisj 12190 |
. . . . . . . . . . . . . 14
|
49 | 26, 31, 48 | mp3an13 1415 |
. . . . . . . . . . . . 13
|
50 | | uneqdifeq 4057 |
. . . . . . . . . . . . 13
|
51 | 47, 49, 50 | sylancr 695 |
. . . . . . . . . . . 12
|
52 | 46, 51 | mpbid 222 |
. . . . . . . . . . 11
|
53 | 52 | eqcomd 2628 |
. . . . . . . . . 10
|
54 | | difeq2 3722 |
. . . . . . . . . . . 12
|
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . 11
|
56 | 55 | rspcev 3309 |
. . . . . . . . . 10
|
57 | 28, 53, 56 | syl2anc 693 |
. . . . . . . . 9
|
58 | | xrex 11829 |
. . . . . . . . . . 11
|
59 | | difexg 4808 |
. . . . . . . . . . 11
|
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . 10
|
61 | 6, 60 | elrnmpti 5376 |
. . . . . . . . 9
|
62 | 57, 61 | sylibr 224 |
. . . . . . . 8
|
63 | 25, 62 | fmpti 6383 |
. . . . . . 7
|
64 | | frn 6053 |
. . . . . . 7
|
65 | 63, 64 | ax-mp 5 |
. . . . . 6
|
66 | | eqid 2622 |
. . . . . . . 8
|
67 | | fnovrn 6809 |
. . . . . . . . . . 11
|
68 | 9, 31, 67 | mp3an13 1415 |
. . . . . . . . . 10
|
69 | | df-ico 12181 |
. . . . . . . . . . . . . . 15
|
70 | | xrlenlt 10103 |
. . . . . . . . . . . . . . 15
|
71 | | xrltletr 11988 |
. . . . . . . . . . . . . . . 16
|
72 | | xrltle 11982 |
. . . . . . . . . . . . . . . . 17
|
73 | 72 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
|
74 | 71, 73 | syld 47 |
. . . . . . . . . . . . . . 15
|
75 | | xrletr 11989 |
. . . . . . . . . . . . . . 15
|
76 | 69, 35, 70, 35, 74, 75 | ixxun 12191 |
. . . . . . . . . . . . . 14
|
77 | 29, 30, 32, 33, 34, 76 | syl32anc 1334 |
. . . . . . . . . . . . 13
|
78 | | uncom 3757 |
. . . . . . . . . . . . 13
|
79 | 77, 78, 45 | 3eqtr3g 2679 |
. . . . . . . . . . . 12
|
80 | | iccssxr 12256 |
. . . . . . . . . . . . 13
|
81 | | incom 3805 |
. . . . . . . . . . . . . 14
|
82 | 69, 35, 70 | ixxdisj 12190 |
. . . . . . . . . . . . . . 15
|
83 | 26, 31, 82 | mp3an13 1415 |
. . . . . . . . . . . . . 14
|
84 | 81, 83 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
85 | | uneqdifeq 4057 |
. . . . . . . . . . . . 13
|
86 | 80, 84, 85 | sylancr 695 |
. . . . . . . . . . . 12
|
87 | 79, 86 | mpbid 222 |
. . . . . . . . . . 11
|
88 | 87 | eqcomd 2628 |
. . . . . . . . . 10
|
89 | | difeq2 3722 |
. . . . . . . . . . . 12
|
90 | 89 | eqeq2d 2632 |
. . . . . . . . . . 11
|
91 | 90 | rspcev 3309 |
. . . . . . . . . 10
|
92 | 68, 88, 91 | syl2anc 693 |
. . . . . . . . 9
|
93 | 6, 60 | elrnmpti 5376 |
. . . . . . . . 9
|
94 | 92, 93 | sylibr 224 |
. . . . . . . 8
|
95 | 66, 94 | fmpti 6383 |
. . . . . . 7
|
96 | | frn 6053 |
. . . . . . 7
|
97 | 95, 96 | ax-mp 5 |
. . . . . 6
|
98 | 65, 97 | unssi 3788 |
. . . . 5
|
99 | | fiss 8330 |
. . . . 5
|
100 | 24, 98, 99 | mp2an 708 |
. . . 4
|
101 | | tgss 20772 |
. . . 4
|
102 | 4, 100, 101 | mp2an 708 |
. . 3
|
103 | 3, 102 | eqsstri 3635 |
. 2
ordTop
|
104 | | letop 21010 |
. . 3
ordTop |
105 | | tgfiss 20795 |
. . 3
ordTop
ordTop
ordTop
|
106 | 104, 23, 105 | mp2an 708 |
. 2
ordTop |
107 | 103, 106 | eqssi 3619 |
1
ordTop |