Step | Hyp | Ref
| Expression |
1 | | letsr 17227 |
. . 3
|
2 | | ledm 17224 |
. . . 4
|
3 | | leordtval.1 |
. . . . 5
|
4 | 3 | leordtvallem1 21014 |
. . . 4
|
5 | | leordtval.2 |
. . . . 5
|
6 | 3, 5 | leordtvallem2 21015 |
. . . 4
|
7 | 2, 4, 6 | ordtval 20993 |
. . 3
ordTop
|
8 | 1, 7 | ax-mp 5 |
. 2
ordTop
|
9 | | snex 4908 |
. . . . 5
|
10 | | xrex 11829 |
. . . . . . 7
|
11 | 10 | pwex 4848 |
. . . . . 6
|
12 | | eqid 2622 |
. . . . . . . . . 10
|
13 | | iocssxr 12257 |
. . . . . . . . . . . 12
|
14 | 10 | elpw2 4828 |
. . . . . . . . . . . 12
|
15 | 13, 14 | mpbir 221 |
. . . . . . . . . . 11
|
16 | 15 | a1i 11 |
. . . . . . . . . 10
|
17 | 12, 16 | fmpti 6383 |
. . . . . . . . 9
|
18 | | frn 6053 |
. . . . . . . . 9
|
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
|
20 | 3, 19 | eqsstri 3635 |
. . . . . . 7
|
21 | | eqid 2622 |
. . . . . . . . . 10
|
22 | | icossxr 12258 |
. . . . . . . . . . . 12
|
23 | 10 | elpw2 4828 |
. . . . . . . . . . . 12
|
24 | 22, 23 | mpbir 221 |
. . . . . . . . . . 11
|
25 | 24 | a1i 11 |
. . . . . . . . . 10
|
26 | 21, 25 | fmpti 6383 |
. . . . . . . . 9
|
27 | | frn 6053 |
. . . . . . . . 9
|
28 | 26, 27 | ax-mp 5 |
. . . . . . . 8
|
29 | 5, 28 | eqsstri 3635 |
. . . . . . 7
|
30 | 20, 29 | unssi 3788 |
. . . . . 6
|
31 | 11, 30 | ssexi 4803 |
. . . . 5
|
32 | 9, 31 | unex 6956 |
. . . 4
|
33 | | ssun2 3777 |
. . . 4
|
34 | | fiss 8330 |
. . . 4
|
35 | 32, 33, 34 | mp2an 708 |
. . 3
|
36 | | fvex 6201 |
. . . . 5
|
37 | | ovex 6678 |
. . . . . . . . . 10
|
38 | | ovex 6678 |
. . . . . . . . . 10
|
39 | 37, 38 | unipr 4449 |
. . . . . . . . 9
|
40 | | iocssxr 12257 |
. . . . . . . . . . 11
|
41 | | icossxr 12258 |
. . . . . . . . . . 11
|
42 | 40, 41 | unssi 3788 |
. . . . . . . . . 10
|
43 | | mnfxr 10096 |
. . . . . . . . . . . . 13
|
44 | | 0xr 10086 |
. . . . . . . . . . . . 13
|
45 | | pnfxr 10092 |
. . . . . . . . . . . . 13
|
46 | | mnflt0 11959 |
. . . . . . . . . . . . . 14
|
47 | | 0lepnf 11966 |
. . . . . . . . . . . . . 14
|
48 | | df-icc 12182 |
. . . . . . . . . . . . . . 15
|
49 | | df-ioc 12180 |
. . . . . . . . . . . . . . 15
|
50 | | xrltnle 10105 |
. . . . . . . . . . . . . . 15
|
51 | | xrletr 11989 |
. . . . . . . . . . . . . . 15
|
52 | | xrlttr 11973 |
. . . . . . . . . . . . . . . 16
|
53 | | xrltle 11982 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
|
55 | 52, 54 | syld 47 |
. . . . . . . . . . . . . . 15
|
56 | 48, 49, 50, 48, 51, 55 | ixxun 12191 |
. . . . . . . . . . . . . 14
|
57 | 46, 47, 56 | mpanr12 721 |
. . . . . . . . . . . . 13
|
58 | 43, 44, 45, 57 | mp3an 1424 |
. . . . . . . . . . . 12
|
59 | | 1re 10039 |
. . . . . . . . . . . . . . 15
|
60 | 59 | rexri 10097 |
. . . . . . . . . . . . . 14
|
61 | | 0lt1 10550 |
. . . . . . . . . . . . . 14
|
62 | | df-ico 12181 |
. . . . . . . . . . . . . . 15
|
63 | | xrlelttr 11987 |
. . . . . . . . . . . . . . 15
|
64 | 62, 48, 63 | ixxss2 12194 |
. . . . . . . . . . . . . 14
|
65 | 60, 61, 64 | mp2an 708 |
. . . . . . . . . . . . 13
|
66 | | unss1 3782 |
. . . . . . . . . . . . 13
|
67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . 12
|
68 | 58, 67 | eqsstr3i 3636 |
. . . . . . . . . . 11
|
69 | | iccmax 12249 |
. . . . . . . . . . 11
|
70 | | uncom 3757 |
. . . . . . . . . . 11
|
71 | 68, 69, 70 | 3sstr3i 3643 |
. . . . . . . . . 10
|
72 | 42, 71 | eqssi 3619 |
. . . . . . . . 9
|
73 | 39, 72 | eqtri 2644 |
. . . . . . . 8
|
74 | | fvex 6201 |
. . . . . . . . 9
|
75 | | ssun1 3776 |
. . . . . . . . . . . 12
|
76 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
77 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | rspcev 3309 |
. . . . . . . . . . . . . . 15
|
80 | 44, 76, 79 | mp2an 708 |
. . . . . . . . . . . . . 14
|
81 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
82 | 12, 81 | elrnmpti 5376 |
. . . . . . . . . . . . . 14
|
83 | 80, 82 | mpbir 221 |
. . . . . . . . . . . . 13
|
84 | 83, 3 | eleqtrri 2700 |
. . . . . . . . . . . 12
|
85 | 75, 84 | sselii 3600 |
. . . . . . . . . . 11
|
86 | | ssun2 3777 |
. . . . . . . . . . . 12
|
87 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
88 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
89 | 88 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
90 | 89 | rspcev 3309 |
. . . . . . . . . . . . . . 15
|
91 | 60, 87, 90 | mp2an 708 |
. . . . . . . . . . . . . 14
|
92 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
93 | 21, 92 | elrnmpti 5376 |
. . . . . . . . . . . . . 14
|
94 | 91, 93 | mpbir 221 |
. . . . . . . . . . . . 13
|
95 | 94, 5 | eleqtrri 2700 |
. . . . . . . . . . . 12
|
96 | 86, 95 | sselii 3600 |
. . . . . . . . . . 11
|
97 | | prssi 4353 |
. . . . . . . . . . 11
|
98 | 85, 96, 97 | mp2an 708 |
. . . . . . . . . 10
|
99 | | ssfii 8325 |
. . . . . . . . . . 11
|
100 | 31, 99 | ax-mp 5 |
. . . . . . . . . 10
|
101 | 98, 100 | sstri 3612 |
. . . . . . . . 9
|
102 | | eltg3i 20765 |
. . . . . . . . 9
|
103 | 74, 101, 102 | mp2an 708 |
. . . . . . . 8
|
104 | 73, 103 | eqeltrri 2698 |
. . . . . . 7
|
105 | | snssi 4339 |
. . . . . . 7
|
106 | 104, 105 | ax-mp 5 |
. . . . . 6
|
107 | | bastg 20770 |
. . . . . . . 8
|
108 | 74, 107 | ax-mp 5 |
. . . . . . 7
|
109 | 100, 108 | sstri 3612 |
. . . . . 6
|
110 | 106, 109 | unssi 3788 |
. . . . 5
|
111 | | fiss 8330 |
. . . . 5
|
112 | 36, 110, 111 | mp2an 708 |
. . . 4
|
113 | | fibas 20781 |
. . . . 5
|
114 | | tgcl 20773 |
. . . . 5
|
115 | | fitop 20705 |
. . . . 5
|
116 | 113, 114,
115 | mp2b 10 |
. . . 4
|
117 | 112, 116 | sseqtri 3637 |
. . 3
|
118 | | 2basgen 20794 |
. . 3
|
119 | 35, 117, 118 | mp2an 708 |
. 2
|
120 | 8, 119 | eqtr4i 2647 |
1
ordTop
|