Step | Hyp | Ref
| Expression |
1 | | hsmexlem4.o |
. . . . . . 7
OrdIso               |
2 | | fveq2 5865 |
. . . . . . . . 9

                  |
3 | 2 | imaeq2d 5168 |
. . . . . . . 8

                          |
4 | | oieq2 8028 |
. . . . . . . 8
                         OrdIso
             OrdIso                |
5 | 3, 4 | syl 17 |
. . . . . . 7

OrdIso              OrdIso                |
6 | 1, 5 | syl5eq 2497 |
. . . . . 6

OrdIso                |
7 | 6 | dmeqd 5037 |
. . . . 5

OrdIso                |
8 | | fveq2 5865 |
. . . . 5

          |
9 | 7, 8 | eleq12d 2523 |
. . . 4

    
OrdIso                     |
10 | 9 | ralbidv 2827 |
. . 3

 
   

OrdIso                     |
11 | | fveq2 5865 |
. . . . . . . . 9
                   |
12 | 11 | imaeq2d 5168 |
. . . . . . . 8
                           |
13 | | oieq2 8028 |
. . . . . . . 8
                        
OrdIso              OrdIso                |
14 | 12, 13 | syl 17 |
. . . . . . 7
 OrdIso              OrdIso                |
15 | 1, 14 | syl5eq 2497 |
. . . . . 6
 OrdIso                |
16 | 15 | dmeqd 5037 |
. . . . 5

OrdIso                |
17 | | fveq2 5865 |
. . . . 5
           |
18 | 16, 17 | eleq12d 2523 |
. . . 4
     
OrdIso                     |
19 | 18 | ralbidv 2827 |
. . 3
  
   

OrdIso                     |
20 | | fveq2 5865 |
. . . . . . . . 9
               
   |
21 | 20 | imaeq2d 5168 |
. . . . . . . 8
                           |
22 | | oieq2 8028 |
. . . . . . . 8
                        
OrdIso              OrdIso                |
23 | 21, 22 | syl 17 |
. . . . . . 7
 OrdIso
             OrdIso          
     |
24 | 1, 23 | syl5eq 2497 |
. . . . . 6

OrdIso          
     |
25 | 24 | dmeqd 5037 |
. . . . 5
 OrdIso                |
26 | | fveq2 5865 |
. . . . 5
       
   |
27 | 25, 26 | eleq12d 2523 |
. . . 4
 
    OrdIso                     |
28 | 27 | ralbidv 2827 |
. . 3
        OrdIso                     |
29 | | imassrn 5179 |
. . . . . . 7
             |
30 | | rankf 8265 |
. . . . . . . 8
          |
31 | | frn 5735 |
. . . . . . . 8
         
  |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
 |
33 | 29, 32 | sstri 3441 |
. . . . . 6
             |
34 | | vex 3048 |
. . . . . . . . 9
 |
35 | | hsmexlem4.u |
. . . . . . . . . 10
            |
36 | 35 | ituni0 8848 |
. . . . . . . . 9
           |
37 | 34, 36 | ax-mp 5 |
. . . . . . . 8
         |
38 | 37 | imaeq2i 5166 |
. . . . . . 7
                 |
39 | | ffun 5731 |
. . . . . . . . . 10
            |
40 | 30, 39 | ax-mp 5 |
. . . . . . . . 9
 |
41 | | wdomimag 8102 |
. . . . . . . . 9
 
     *   |
42 | 40, 34, 41 | mp2an 678 |
. . . . . . . 8
    *  |
43 | | sneq 3978 |
. . . . . . . . . . . . 13
       |
44 | 43 | fveq2d 5869 |
. . . . . . . . . . . 12
               |
45 | 44 | raleqdv 2993 |
. . . . . . . . . . 11
  
      
           |
46 | | hsmexlem4.s |
. . . . . . . . . . 11
                |
47 | 45, 46 | elrab2 3198 |
. . . . . . . . . 10

     
           |
48 | 47 | simprbi 466 |
. . . . . . . . 9
           |
49 | | snex 4641 |
. . . . . . . . . . . 12
   |
50 | | tcid 8223 |
. . . . . . . . . . . 12
             |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
 
       |
52 | | ssnid 3997 |
. . . . . . . . . . 11
   |
53 | 51, 52 | sselii 3429 |
. . . . . . . . . 10
       |
54 | | breq1 4405 |
. . . . . . . . . . 11
 
   |
55 | 54 | rspcv 3146 |
. . . . . . . . . 10
               
   |
56 | 53, 55 | ax-mp 5 |
. . . . . . . . 9
 
         |
57 | | domwdom 8089 |
. . . . . . . . 9

*   |
58 | 48, 56, 57 | 3syl 18 |
. . . . . . . 8
 *   |
59 | | wdomtr 8090 |
. . . . . . . 8
      * * 
    *   |
60 | 42, 58, 59 | sylancr 669 |
. . . . . . 7
     *   |
61 | 38, 60 | syl5eqbr 4436 |
. . . . . 6
             *   |
62 | | eqid 2451 |
. . . . . . 7
OrdIso              OrdIso               |
63 | 62 | hsmexlem1 8856 |
. . . . . 6
             
            *  OrdIso              har     |
64 | 33, 61, 63 | sylancr 669 |
. . . . 5
 OrdIso              har     |
65 | | hsmexlem4.h |
. . . . . 6
    har       har      |
66 | 65 | hsmexlem7 8853 |
. . . . 5
    har    |
67 | 64, 66 | syl6eleqr 2540 |
. . . 4
 OrdIso                    |
68 | 67 | rgen 2747 |
. . 3

OrdIso                   |
69 | | nfra1 2769 |
. . . . . 6
   OrdIso                   |
70 | | nfv 1761 |
. . . . . 6
  |
71 | 69, 70 | nfan 2011 |
. . . . 5
   
OrdIso                 
  |
72 | 35 | ituniiun 8852 |
. . . . . . . . . . . . 13
                    |
73 | 34, 72 | ax-mp 5 |
. . . . . . . . . . . 12
      
           |
74 | 73 | imaeq2i 5166 |
. . . . . . . . . . 11
               
          |
75 | | imaiun 6150 |
. . . . . . . . . . 11
             
             |
76 | 74, 75 | eqtri 2473 |
. . . . . . . . . 10
                          |
77 | | oieq2 8028 |
. . . . . . . . . 10
                         
OrdIso          
   OrdIso                 |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . 9
OrdIso              OrdIso                |
79 | 78 | dmeqi 5036 |
. . . . . . . 8
OrdIso              OrdIso 
              |
80 | 58 | ad2antll 735 |
. . . . . . . . 9
   OrdIso                  
 
*   |
81 | 65 | hsmexlem9 8855 |
. . . . . . . . . 10
       |
82 | 81 | ad2antrl 734 |
. . . . . . . . 9
   OrdIso                  
 
      |
83 | | ssrab2 3514 |
. . . . . . . . . . . . . . . . . . 19
              
      |
84 | 46, 83 | eqsstri 3462 |
. . . . . . . . . . . . . . . . . 18
      |
85 | 84 | sseli 3428 |
. . . . . . . . . . . . . . . . 17
        |
86 | | r1elssi 8276 |
. . . . . . . . . . . . . . . . 17
     
       |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
        |
88 | 87 | sselda 3432 |
. . . . . . . . . . . . . . 15
 
        |
89 | | snssi 4116 |
. . . . . . . . . . . . . . . . . . 19
  
  |
90 | 34 | tcss 8228 |
. . . . . . . . . . . . . . . . . . 19
               |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      
      |
92 | 49 | tcel 8229 |
. . . . . . . . . . . . . . . . . . 19
               |
93 | 52, 92 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
             |
94 | 91, 93 | sstrd 3442 |
. . . . . . . . . . . . . . . . 17
      
        |
95 | | ssralv 3493 |
. . . . . . . . . . . . . . . . 17
            
 
                  |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
  
       
          |
97 | 48, 96 | mpan9 472 |
. . . . . . . . . . . . . . 15
 
           |
98 | | sneq 3978 |
. . . . . . . . . . . . . . . . . 18
       |
99 | 98 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
               |
100 | 99 | raleqdv 2993 |
. . . . . . . . . . . . . . . 16
  
      
           |
101 | 100, 46 | elrab2 3198 |
. . . . . . . . . . . . . . 15

     
           |
102 | 88, 97, 101 | sylanbrc 670 |
. . . . . . . . . . . . . 14
 
   |
103 | 102 | adantll 720 |
. . . . . . . . . . . . 13
    
  |
104 | 103 | adantll 720 |
. . . . . . . . . . . 12
   
OrdIso                        |
105 | | simpll 760 |
. . . . . . . . . . . 12
   
OrdIso                      
OrdIso                    |
106 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
           |
107 | 106 | fveq1d 5867 |
. . . . . . . . . . . . . . . . 17
                   |
108 | 107 | imaeq2d 5168 |
. . . . . . . . . . . . . . . 16
                           |
109 | | oieq2 8028 |
. . . . . . . . . . . . . . . 16
                        
OrdIso              OrdIso                |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . 15
 OrdIso              OrdIso                |
111 | 110 | dmeqd 5037 |
. . . . . . . . . . . . . 14
 OrdIso             
OrdIso                |
112 | 111 | eleq1d 2513 |
. . . . . . . . . . . . 13
  OrdIso                 
OrdIso                     |
113 | 112 | rspcv 3146 |
. . . . . . . . . . . 12
  
OrdIso                  OrdIso                     |
114 | 104, 105,
113 | sylc 62 |
. . . . . . . . . . 11
   
OrdIso                      OrdIso                    |
115 | | imassrn 5179 |
. . . . . . . . . . . . 13
             |
116 | 115, 32 | sstri 3441 |
. . . . . . . . . . . 12
             |
117 | | fvex 5875 |
. . . . . . . . . . . . . . 15
         |
118 | 117 | funimaex 5661 |
. . . . . . . . . . . . . 14
               |
119 | 40, 118 | ax-mp 5 |
. . . . . . . . . . . . 13
             |
120 | 119 | elpw 3957 |
. . . . . . . . . . . 12
             
              |
121 | 116, 120 | mpbir 213 |
. . . . . . . . . . 11
              |
122 | 114, 121 | jctil 540 |
. . . . . . . . . 10
   
OrdIso                                    OrdIso                     |
123 | 122 | ralrimiva 2802 |
. . . . . . . . 9
   OrdIso                  
 

              OrdIso                     |
124 | | eqid 2451 |
. . . . . . . . . 10
OrdIso              OrdIso               |
125 | | eqid 2451 |
. . . . . . . . . 10
OrdIso               OrdIso                |
126 | 124, 125 | hsmexlem3 8858 |
. . . . . . . . 9
   *      
              OrdIso                   
OrdIso 
             har           |
127 | 80, 82, 123, 126 | syl21anc 1267 |
. . . . . . . 8
   OrdIso                  
 
OrdIso               har           |
128 | 79, 127 | syl5eqel 2533 |
. . . . . . 7
   OrdIso                  
 
OrdIso              har           |
129 | 65 | hsmexlem8 8854 |
. . . . . . . 8
     har  
        |
130 | 129 | ad2antrl 734 |
. . . . . . 7
   OrdIso                  
 
    har           |
131 | 128, 130 | eleqtrrd 2532 |
. . . . . 6
   OrdIso                  
 
OrdIso                    |
132 | 131 | expr 620 |
. . . . 5
   OrdIso                    OrdIso                     |
133 | 71, 132 | ralrimi 2788 |
. . . 4
   OrdIso                   
OrdIso                    |
134 | 133 | expcom 437 |
. . 3
  
OrdIso                  
OrdIso                     |
135 | 10, 19, 28, 68, 134 | finds1 6722 |
. 2
 
      |
136 | 135 | r19.21bi 2757 |
1
 
       |