Step | Hyp | Ref
| Expression |
1 | | elpwi 3960 |
. . . . . 6
    |
2 | 1 | adantr 467 |
. . . . 5
  

  |
3 | 2 | ralimi 2781 |
. . . 4
 




  |
4 | | iunss 4319 |
. . . 4
 
   |
5 | 3, 4 | sylibr 216 |
. . 3
 



   |
6 | 5 | 3ad2ant3 1031 |
. 2
 



  
  |
7 | | xpexg 6593 |
. . . 4
 
     |
8 | 7 | 3adant3 1028 |
. . 3
 



      |
9 | | nfv 1761 |
. . . . . . . . 9
  |
10 | | nfra1 2769 |
. . . . . . . . 9
   
   |
11 | 9, 10 | nfan 2011 |
. . . . . . . 8
    
    |
12 | | rsp 2754 |
. . . . . . . . 9
 




      |
13 | | onelss 5465 |
. . . . . . . . . . . . . 14
 
   |
14 | 13 | imp 431 |
. . . . . . . . . . . . 13
  
  |
15 | 14 | adantrl 722 |
. . . . . . . . . . . 12
  
  
  |
16 | 15 | 3adant3 1028 |
. . . . . . . . . . 11
  
     |
17 | | hsmexlem.f |
. . . . . . . . . . . . . . . . . . 19
OrdIso   |
18 | 17 | oismo 8055 |
. . . . . . . . . . . . . . . . . 18


   |
19 | 1, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
      |
20 | 19 | ad2antrl 734 |
. . . . . . . . . . . . . . . 16
  
   
   |
21 | 20 | simprd 465 |
. . . . . . . . . . . . . . 15
  
     |
22 | 17 | oif 8045 |
. . . . . . . . . . . . . . 15
     |
23 | 21, 22 | jctil 540 |
. . . . . . . . . . . . . 14
  
           |
24 | | dffo2 5797 |
. . . . . . . . . . . . . 14
             |
25 | 23, 24 | sylibr 216 |
. . . . . . . . . . . . 13
  
         |
26 | | dffo3 6037 |
. . . . . . . . . . . . . 14
           
       |
27 | 26 | simprbi 466 |
. . . . . . . . . . . . 13
      
      |
28 | | rsp 2754 |
. . . . . . . . . . . . 13
 

     
       |
29 | 25, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
  
            |
30 | 29 | 3impia 1205 |
. . . . . . . . . . 11
  
          |
31 | | ssrexv 3494 |
. . . . . . . . . . 11

      
       |
32 | 16, 30, 31 | sylc 62 |
. . . . . . . . . 10
  
   
      |
33 | 32 | 3exp 1207 |
. . . . . . . . 9
      
        |
34 | 12, 33 | sylan9r 664 |
. . . . . . . 8
    
    
        |
35 | 11, 34 | reximdai 2856 |
. . . . . . 7
    
   
 
       |
36 | 35 | 3adant1 1026 |
. . . . . 6
 



   
 
       |
37 | | nfv 1761 |
. . . . . . 7
  
     |
38 | | nfcv 2592 |
. . . . . . . 8
   |
39 | | nfcv 2592 |
. . . . . . . . . . 11
  |
40 | | nfcsb1v 3379 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
41 | 39, 40 | nfoi 8029 |
. . . . . . . . . 10
 OrdIso
  ![]_ ]_](_urbrack.gif)   |
42 | | nfcv 2592 |
. . . . . . . . . 10
   |
43 | 41, 42 | nffv 5872 |
. . . . . . . . 9
  OrdIso 
 ![]_ ]_](_urbrack.gif)      |
44 | 43 | nfeq2 2607 |
. . . . . . . 8
 OrdIso   ![]_ ]_](_urbrack.gif)      |
45 | 38, 44 | nfrex 2850 |
. . . . . . 7
  
OrdIso   ![]_ ]_](_urbrack.gif)      |
46 | | csbeq1a 3372 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
47 | | oieq2 8028 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif) OrdIso  OrdIso   ![]_ ]_](_urbrack.gif)    |
48 | 46, 47 | syl 17 |
. . . . . . . . . . 11
 OrdIso  OrdIso   ![]_ ]_](_urbrack.gif)    |
49 | 17, 48 | syl5eq 2497 |
. . . . . . . . . 10
 OrdIso   ![]_ ]_](_urbrack.gif)    |
50 | 49 | fveq1d 5867 |
. . . . . . . . 9
     OrdIso 
 ![]_ ]_](_urbrack.gif)       |
51 | 50 | eqeq2d 2461 |
. . . . . . . 8
     
OrdIso   ![]_ ]_](_urbrack.gif)        |
52 | 51 | rexbidv 2901 |
. . . . . . 7
  
   

OrdIso   ![]_ ]_](_urbrack.gif)        |
53 | 37, 45, 52 | cbvrex 3016 |
. . . . . 6
  
   


OrdIso   ![]_ ]_](_urbrack.gif)       |
54 | 36, 53 | syl6ib 230 |
. . . . 5
 



   
 
OrdIso 
 ![]_ ]_](_urbrack.gif)        |
55 | | eliun 4283 |
. . . . 5
 

  |
56 | | vex 3048 |
. . . . . . . . . . 11
 |
57 | | vex 3048 |
. . . . . . . . . . 11
 |
58 | 56, 57 | op1std 6803 |
. . . . . . . . . 10
          |
59 | 58 | csbeq1d 3370 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
60 | | oieq2 8028 |
. . . . . . . . 9
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
OrdIso       ![]_ ]_](_urbrack.gif)  OrdIso   ![]_ ]_](_urbrack.gif)    |
61 | 59, 60 | syl 17 |
. . . . . . . 8
    OrdIso
      ![]_ ]_](_urbrack.gif) 
OrdIso 
 ![]_ ]_](_urbrack.gif)    |
62 | 56, 57 | op2ndd 6804 |
. . . . . . . 8
          |
63 | 61, 62 | fveq12d 5871 |
. . . . . . 7
    OrdIso       ![]_ ]_](_urbrack.gif)         OrdIso   ![]_ ]_](_urbrack.gif)       |
64 | 63 | eqeq2d 2461 |
. . . . . 6
     OrdIso       ![]_ ]_](_urbrack.gif)         OrdIso   ![]_ ]_](_urbrack.gif)        |
65 | 64 | rexxp 4977 |
. . . . 5
     OrdIso       ![]_ ]_](_urbrack.gif)         

OrdIso   ![]_ ]_](_urbrack.gif)       |
66 | 54, 55, 65 | 3imtr4g 274 |
. . . 4
 



   
    OrdIso       ![]_ ]_](_urbrack.gif)            |
67 | 66 | imp 431 |
. . 3
     
        OrdIso       ![]_ ]_](_urbrack.gif)           |
68 | 8, 67 | wdomd 8096 |
. 2
 



  
*     |
69 | | hsmexlem.g |
. . 3
OrdIso 
  |
70 | 69 | hsmexlem1 8856 |
. 2
   
*   
har       |
71 | 6, 68, 70 | syl2anc 667 |
1
 



  har  
    |