Step | Hyp | Ref
| Expression |
1 | | eqid 2453 |
. . . 4
     
     |
2 | | eqid 2453 |
. . . 4
           |
3 | 1, 2 | leordtval2 20240 |
. . 3
ordTop                      |
4 | | fvex 5880 |
. . . 4
  
  |
5 | | fvex 5880 |
. . . . . 6
ordTop  |
6 | | lecldbas.1 |
. . . . . . . 8
 
   |
7 | | iccf 11740 |
. . . . . . . . . . 11
![[,] [,]](_icc.gif)  
     |
8 | | ffn 5733 |
. . . . . . . . . . 11
 ![[,] [,]](_icc.gif)      
    |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
   |
10 | | ovelrn 6450 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif)     |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9

    ![[,] [,]](_icc.gif)    |
12 | | difeq2 3547 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)     |
13 | | iccordt 20242 |
. . . . . . . . . . . . 13
  ![[,] [,]](_icc.gif)     ordTop   |
14 | | letopuni 20235 |
. . . . . . . . . . . . . 14
 ordTop
 |
15 | 14 | cldopn 20058 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)     ordTop     ![[,] [,]](_icc.gif)   ordTop
  |
16 | 13, 15 | ax-mp 5 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)   ordTop  |
17 | 12, 16 | syl6eqel 2539 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    ordTop
  |
18 | 17 | rexlimivw 2878 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    ordTop
  |
19 | 18 | rexlimivw 2878 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)    ordTop   |
20 | 11, 19 | sylbi 199 |
. . . . . . . 8
 
 ordTop
  |
21 | 6, 20 | fmpti 6050 |
. . . . . . 7
  ![[,] [,]](_icc.gif)  ordTop
 |
22 | | frn 5740 |
. . . . . . 7
   ![[,] [,]](_icc.gif)  ordTop
ordTop
  |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
ordTop
 |
24 | 5, 23 | ssexi 4551 |
. . . . 5
 |
25 | | eqid 2453 |
. . . . . . . 8

          |
26 | | mnfxr 11421 |
. . . . . . . . . . 11
 |
27 | | fnovrn 6449 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)  ![[,] [,]](_icc.gif)  |
28 | 9, 26, 27 | mp3an12 1356 |
. . . . . . . . . 10

 ![[,] [,]](_icc.gif)  ![[,] [,]](_icc.gif)  |
29 | 26 | a1i 11 |
. . . . . . . . . . . . . 14

  |
30 | | id 22 |
. . . . . . . . . . . . . 14

  |
31 | | pnfxr 11419 |
. . . . . . . . . . . . . . 15
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14

  |
33 | | mnfle 11442 |
. . . . . . . . . . . . . 14

  |
34 | | pnfge 11439 |
. . . . . . . . . . . . . 14

  |
35 | | df-icc 11649 |
. . . . . . . . . . . . . . 15
  

    |
36 | | df-ioc 11647 |
. . . . . . . . . . . . . . 15
  

    |
37 | | xrltnle 9706 |
. . . . . . . . . . . . . . 15
   
   |
38 | | xrletr 11462 |
. . . . . . . . . . . . . . 15
  
 
    |
39 | | xrlelttr 11460 |
. . . . . . . . . . . . . . . 16
  
    |
40 | | xrltle 11455 |
. . . . . . . . . . . . . . . . 17
     |
41 | 40 | 3adant2 1028 |
. . . . . . . . . . . . . . . 16
     |
42 | 39, 41 | syld 45 |
. . . . . . . . . . . . . . 15
  
    |
43 | 35, 36, 37, 35, 38, 42 | ixxun 11658 |
. . . . . . . . . . . . . 14
       ![[,] [,]](_icc.gif)   
      |
44 | 29, 30, 32, 33, 34, 43 | syl32anc 1277 |
. . . . . . . . . . . . 13

  ![[,] [,]](_icc.gif)          |
45 | | iccmax 11717 |
. . . . . . . . . . . . 13
   |
46 | 44, 45 | syl6eq 2503 |
. . . . . . . . . . . 12

  ![[,] [,]](_icc.gif)        |
47 | | iccssxr 11724 |
. . . . . . . . . . . . 13
 ![[,] [,]](_icc.gif)   |
48 | 35, 36, 37 | ixxdisj 11657 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        |
49 | 26, 31, 48 | mp3an13 1357 |
. . . . . . . . . . . . 13

  ![[,] [,]](_icc.gif)        |
50 | | uneqdifeq 3858 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
51 | 47, 49, 50 | sylancr 670 |
. . . . . . . . . . . 12

   ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)         |
52 | 46, 51 | mpbid 214 |
. . . . . . . . . . 11

  ![[,] [,]](_icc.gif)        |
53 | 52 | eqcomd 2459 |
. . . . . . . . . 10

   
 ![[,] [,]](_icc.gif)     |
54 | | difeq2 3547 |
. . . . . . . . . . . 12
  ![[,] [,]](_icc.gif)    
 ![[,] [,]](_icc.gif)     |
55 | 54 | eqeq2d 2463 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)     
 
   
 ![[,] [,]](_icc.gif)      |
56 | 55 | rspcev 3152 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    
![[,] [,]](_icc.gif)   
    |
57 | 28, 53, 56 | syl2anc 667 |
. . . . . . . . 9

 ![[,] [,]](_icc.gif)    
   |
58 | | xrex 11306 |
. . . . . . . . . . 11
 |
59 | | difexg 4554 |
. . . . . . . . . . 11

    |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . 10
   |
61 | 6, 60 | elrnmpti 5088 |
. . . . . . . . 9
   
 ![[,] [,]](_icc.gif)    
   |
62 | 57, 61 | sylibr 216 |
. . . . . . . 8

     |
63 | 25, 62 | fmpti 6050 |
. . . . . . 7

         |
64 | | frn 5740 |
. . . . . . 7
                 |
65 | 63, 64 | ax-mp 5 |
. . . . . 6
    
 |
66 | | eqid 2453 |
. . . . . . . 8

          |
67 | | fnovrn 6449 |
. . . . . . . . . . 11
    
   ![[,] [,]](_icc.gif)  |
68 | 9, 31, 67 | mp3an13 1357 |
. . . . . . . . . 10

   ![[,] [,]](_icc.gif)  |
69 | | df-ico 11648 |
. . . . . . . . . . . . . . 15
  

    |
70 | | xrlenlt 9704 |
. . . . . . . . . . . . . . 15
   
   |
71 | | xrltletr 11461 |
. . . . . . . . . . . . . . . 16
  
 
    |
72 | | xrltle 11455 |
. . . . . . . . . . . . . . . . 17
   
   |
73 | 72 | 3adant2 1028 |
. . . . . . . . . . . . . . . 16
  

   |
74 | 71, 73 | syld 45 |
. . . . . . . . . . . . . . 15
  
 
    |
75 | | xrletr 11462 |
. . . . . . . . . . . . . . 15
  
    |
76 | 69, 35, 70, 35, 74, 75 | ixxun 11658 |
. . . . . . . . . . . . . 14
          
      |
77 | 29, 30, 32, 33, 34, 76 | syl32anc 1277 |
. . . . . . . . . . . . 13

            |
78 | | uncom 3580 |
. . . . . . . . . . . . 13
           
     |
79 | 77, 78, 45 | 3eqtr3g 2510 |
. . . . . . . . . . . 12

   
      |
80 | | iccssxr 11724 |
. . . . . . . . . . . . 13
    |
81 | | incom 3627 |
. . . . . . . . . . . . . 14
   
       
     |
82 | 69, 35, 70 | ixxdisj 11657 |
. . . . . . . . . . . . . . 15
 
          |
83 | 26, 31, 82 | mp3an13 1357 |
. . . . . . . . . . . . . 14

          |
84 | 81, 83 | syl5eq 2499 |
. . . . . . . . . . . . 13

   
      |
85 | | uneqdifeq 3858 |
. . . . . . . . . . . . 13
    
        
    
    
 
        |
86 | 80, 84, 85 | sylancr 670 |
. . . . . . . . . . . 12

    
    
 
        |
87 | 79, 86 | mpbid 214 |
. . . . . . . . . . 11

          |
88 | 87 | eqcomd 2459 |
. . . . . . . . . 10

   
      |
89 | | difeq2 3547 |
. . . . . . . . . . . 12
   
  
      |
90 | 89 | eqeq2d 2463 |
. . . . . . . . . . 11
   
         
       |
91 | 90 | rspcev 3152 |
. . . . . . . . . 10
    
     
    ![[,] [,]](_icc.gif)    
   |
92 | 68, 88, 91 | syl2anc 667 |
. . . . . . . . 9

 ![[,] [,]](_icc.gif)    
   |
93 | 6, 60 | elrnmpti 5088 |
. . . . . . . . 9
   
 ![[,] [,]](_icc.gif)    
   |
94 | 92, 93 | sylibr 216 |
. . . . . . . 8

     |
95 | 66, 94 | fmpti 6050 |
. . . . . . 7

       
 |
96 | | frn 5740 |
. . . . . . 7
         
    
  |
97 | 95, 96 | ax-mp 5 |
. . . . . 6
      |
98 | 65, 97 | unssi 3611 |
. . . . 5
             |
99 | | fiss 7943 |
. . . . 5
   
    
    
                       |
100 | 24, 98, 99 | mp2an 679 |
. . . 4
         
     
     |
101 | | tgss 19996 |
. . . 4
                                                         |
102 | 4, 100, 101 | mp2an 679 |
. . 3
                             |
103 | 3, 102 | eqsstri 3464 |
. 2
ordTop
         |
104 | | letop 20234 |
. . 3
ordTop  |
105 | | tgfiss 20019 |
. . 3
  ordTop
ordTop
         ordTop
  |
106 | 104, 23, 105 | mp2an 679 |
. 2
        ordTop  |
107 | 103, 106 | eqssi 3450 |
1
ordTop          |