Step | Hyp | Ref
| Expression |
1 | | elqsi 6094 |
. . . . . . . 8
    
   ![]](rbrack.gif)   |
2 | | eropr.1 |
. . . . . . . 8
     |
3 | 1, 2 | eleq2s 2129 |
. . . . . . 7
 
  ![]](rbrack.gif)   |
4 | | elqsi 6094 |
. . . . . . . 8
    
   ![]](rbrack.gif)   |
5 | | eropr.2 |
. . . . . . . 8
     |
6 | 4, 5 | eleq2s 2129 |
. . . . . . 7
 
  ![]](rbrack.gif)   |
7 | 3, 6 | anim12i 321 |
. . . . . 6
 
     ![]](rbrack.gif) 
  ![]](rbrack.gif)    |
8 | 7 | adantl 262 |
. . . . 5
      
  ![]](rbrack.gif)
   ![]](rbrack.gif)    |
9 | | reeanv 2473 |
. . . . 5
 
    ![]](rbrack.gif)
  ![]](rbrack.gif)   
  ![]](rbrack.gif) 
  ![]](rbrack.gif)    |
10 | 8, 9 | sylibr 137 |
. . . 4
     


  ![]](rbrack.gif)   ![]](rbrack.gif)    |
11 | | eropr.3 |
. . . . . . . 8
   |
12 | 11 | adantr 261 |
. . . . . . 7
       |
13 | | ecexg 6046 |
. . . . . . 7
  
  ![]](rbrack.gif)   |
14 | | elisset 2562 |
. . . . . . 7
  
  ![]](rbrack.gif)      ![]](rbrack.gif)   |
15 | 12, 13, 14 | 3syl 17 |
. . . . . 6
     
    ![]](rbrack.gif)   |
16 | 15 | biantrud 288 |
. . . . 5
         ![]](rbrack.gif)   ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)  
 
  ![]](rbrack.gif)     |
17 | 16 | 2rexbidv 2343 |
. . . 4
       

  ![]](rbrack.gif)   ![]](rbrack.gif)   
    ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif)     |
18 | 10, 17 | mpbid 135 |
. . 3
     

    ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif)    |
19 | | 19.42v 1783 |
. . . . . . . 8
       ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)  
 
  ![]](rbrack.gif)    |
20 | 19 | bicomi 123 |
. . . . . . 7
     ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif) 
      ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
21 | 20 | rexbii 2325 |
. . . . . 6
 
 
  ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif) 
       ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
22 | | rexcom4 2571 |
. . . . . 6
 
      ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    
    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
23 | 21, 22 | bitri 173 |
. . . . 5
 
 
  ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif) 
  
    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
24 | 23 | rexbii 2325 |
. . . 4
 
     ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif)     
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
25 | | rexcom4 2571 |
. . . 4
 
  
    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    

    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
26 | 24, 25 | bitri 173 |
. . 3
 
     ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif)    

    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
27 | 18, 26 | sylib 127 |
. 2
             ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)    |
28 | | reeanv 2473 |
. . . . . 6
 
       ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)          ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)     |
29 | | eceq1 6077 |
. . . . . . . . . . 11
   ![]](rbrack.gif)   ![]](rbrack.gif)   |
30 | 29 | eqeq2d 2048 |
. . . . . . . . . 10
 
  ![]](rbrack.gif)
  ![]](rbrack.gif)    |
31 | 30 | anbi1d 438 |
. . . . . . . . 9
  
  ![]](rbrack.gif)   ![]](rbrack.gif)     ![]](rbrack.gif)
  ![]](rbrack.gif)     |
32 | | oveq1 5462 |
. . . . . . . . . . 11
       |
33 | 32 | eceq1d 6078 |
. . . . . . . . . 10
  
  ![]](rbrack.gif)  
  ![]](rbrack.gif)   |
34 | 33 | eqeq2d 2048 |
. . . . . . . . 9
 
    ![]](rbrack.gif)  
  ![]](rbrack.gif)    |
35 | 31, 34 | anbi12d 442 |
. . . . . . . 8
      ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)   
  ![]](rbrack.gif)     |
36 | | eceq1 6077 |
. . . . . . . . . . 11
   ![]](rbrack.gif)   ![]](rbrack.gif)   |
37 | 36 | eqeq2d 2048 |
. . . . . . . . . 10
 
  ![]](rbrack.gif)
  ![]](rbrack.gif)    |
38 | 37 | anbi2d 437 |
. . . . . . . . 9
  
  ![]](rbrack.gif)
  ![]](rbrack.gif)     ![]](rbrack.gif)   ![]](rbrack.gif)     |
39 | | oveq2 5463 |
. . . . . . . . . . 11
 
     |
40 | 39 | eceq1d 6078 |
. . . . . . . . . 10
  
  ![]](rbrack.gif)  
  ![]](rbrack.gif)   |
41 | 40 | eqeq2d 2048 |
. . . . . . . . 9
 
 
  ![]](rbrack.gif)
    ![]](rbrack.gif)    |
42 | 38, 41 | anbi12d 442 |
. . . . . . . 8
      ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)     |
43 | 35, 42 | cbvrex2v 2536 |
. . . . . . 7
 
     ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)        ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
44 | | eceq1 6077 |
. . . . . . . . . . 11
   ![]](rbrack.gif)   ![]](rbrack.gif)   |
45 | 44 | eqeq2d 2048 |
. . . . . . . . . 10
 
  ![]](rbrack.gif)
  ![]](rbrack.gif)    |
46 | 45 | anbi1d 438 |
. . . . . . . . 9
  
  ![]](rbrack.gif)   ![]](rbrack.gif)     ![]](rbrack.gif)
  ![]](rbrack.gif)     |
47 | | oveq1 5462 |
. . . . . . . . . . 11
       |
48 | 47 | eceq1d 6078 |
. . . . . . . . . 10
  
  ![]](rbrack.gif)  
  ![]](rbrack.gif)   |
49 | 48 | eqeq2d 2048 |
. . . . . . . . 9
 
    ![]](rbrack.gif)  
  ![]](rbrack.gif)    |
50 | 46, 49 | anbi12d 442 |
. . . . . . . 8
      ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)   
  ![]](rbrack.gif)     |
51 | | eceq1 6077 |
. . . . . . . . . . 11
   ![]](rbrack.gif)   ![]](rbrack.gif)   |
52 | 51 | eqeq2d 2048 |
. . . . . . . . . 10
 
  ![]](rbrack.gif)
  ![]](rbrack.gif)    |
53 | 52 | anbi2d 437 |
. . . . . . . . 9
  
  ![]](rbrack.gif)
  ![]](rbrack.gif)     ![]](rbrack.gif)   ![]](rbrack.gif)     |
54 | | oveq2 5463 |
. . . . . . . . . . 11
 
     |
55 | 54 | eceq1d 6078 |
. . . . . . . . . 10
  
  ![]](rbrack.gif)  
  ![]](rbrack.gif)   |
56 | 55 | eqeq2d 2048 |
. . . . . . . . 9
 
 
  ![]](rbrack.gif)
    ![]](rbrack.gif)    |
57 | 53, 56 | anbi12d 442 |
. . . . . . . 8
      ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)     |
58 | 50, 57 | cbvrex2v 2536 |
. . . . . . 7
 
     ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)        ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)    |
59 | 43, 58 | anbi12i 433 |
. . . . . 6
  

    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)          ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)     |
60 | 28, 59 | bitr4i 176 |
. . . . 5
 
       ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)          ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)     |
61 | | reeanv 2473 |
. . . . . . 7
 
      ![]](rbrack.gif)
  ![]](rbrack.gif)   
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)         ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)     |
62 | | eropr.11 |
. . . . . . . . . . . . . 14
     
  
                |
63 | | eropr.4 |
. . . . . . . . . . . . . . . . 17
   |
64 | 63 | adantr 261 |
. . . . . . . . . . . . . . . 16
     
  
  |
65 | | eropr.7 |
. . . . . . . . . . . . . . . . . 18

  |
66 | 65 | adantr 261 |
. . . . . . . . . . . . . . . . 17
     
  
  |
67 | | simprll 489 |
. . . . . . . . . . . . . . . . 17
     
  
  |
68 | 66, 67 | sseldd 2940 |
. . . . . . . . . . . . . . . 16
     
  
  |
69 | 64, 68 | erth 6086 |
. . . . . . . . . . . . . . 15
     
  
     ![]](rbrack.gif)
  ![]](rbrack.gif)    |
70 | | eropr.5 |
. . . . . . . . . . . . . . . . 17
   |
71 | 70 | adantr 261 |
. . . . . . . . . . . . . . . 16
     
  
  |
72 | | eropr.8 |
. . . . . . . . . . . . . . . . . 18

  |
73 | 72 | adantr 261 |
. . . . . . . . . . . . . . . . 17
     
  
  |
74 | | simprrl 491 |
. . . . . . . . . . . . . . . . 17
     
  
  |
75 | 73, 74 | sseldd 2940 |
. . . . . . . . . . . . . . . 16
     
  
  |
76 | 71, 75 | erth 6086 |
. . . . . . . . . . . . . . 15
     
  
     ![]](rbrack.gif)
  ![]](rbrack.gif)    |
77 | 69, 76 | anbi12d 442 |
. . . . . . . . . . . . . 14
     
  
          ![]](rbrack.gif)   ![]](rbrack.gif)
  ![]](rbrack.gif)
  ![]](rbrack.gif)     |
78 | | eropr.6 |
. . . . . . . . . . . . . . . 16
   |
79 | 78 | adantr 261 |
. . . . . . . . . . . . . . 15
     
  
  |
80 | | eropr.9 |
. . . . . . . . . . . . . . . . 17

  |
81 | 80 | adantr 261 |
. . . . . . . . . . . . . . . 16
     
  
  |
82 | | eropr.10 |
. . . . . . . . . . . . . . . . . 18
        |
83 | 82 | adantr 261 |
. . . . . . . . . . . . . . . . 17
     
  
 
     |
84 | 83, 67, 74 | fovrnd 5587 |
. . . . . . . . . . . . . . . 16
     
  

   |
85 | 81, 84 | sseldd 2940 |
. . . . . . . . . . . . . . 15
     
  

   |
86 | 79, 85 | erth 6086 |
. . . . . . . . . . . . . 14
     
  
 
    
 
  ![]](rbrack.gif)
 
  ![]](rbrack.gif)    |
87 | 62, 77, 86 | 3imtr3d 191 |
. . . . . . . . . . . . 13
     
  
    ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)      ![]](rbrack.gif)
 
  ![]](rbrack.gif)    |
88 | | eqeq2 2046 |
. . . . . . . . . . . . . 14
     ![]](rbrack.gif)   
  ![]](rbrack.gif)
    ![]](rbrack.gif)  
  ![]](rbrack.gif)    |
89 | 88 | biimprcd 149 |
. . . . . . . . . . . . 13
  
  ![]](rbrack.gif)  
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)
 
  ![]](rbrack.gif)
   |
90 | 87, 89 | syl6 29 |
. . . . . . . . . . . 12
     
  
    ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)       ![]](rbrack.gif)  
  ![]](rbrack.gif)     |
91 | 90 | impd 242 |
. . . . . . . . . . 11
     
  
     ![]](rbrack.gif)   ![]](rbrack.gif)
  ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)   
  ![]](rbrack.gif)    |
92 | | eqeq1 2043 |
. . . . . . . . . . . . . . 15
   ![]](rbrack.gif)    ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
93 | | eqeq1 2043 |
. . . . . . . . . . . . . . 15
   ![]](rbrack.gif)    ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
94 | 92, 93 | bi2anan9 538 |
. . . . . . . . . . . . . 14
    ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)   ![]](rbrack.gif)     ![]](rbrack.gif)   ![]](rbrack.gif)
  ![]](rbrack.gif)
  ![]](rbrack.gif)     |
95 | 94 | anbi1d 438 |
. . . . . . . . . . . . 13
    ![]](rbrack.gif)
  ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)      ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)     |
96 | 95 | adantr 261 |
. . . . . . . . . . . 12
     ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)      ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)     |
97 | | eqeq1 2043 |
. . . . . . . . . . . . 13
     ![]](rbrack.gif)      ![]](rbrack.gif)
   |
98 | 97 | adantl 262 |
. . . . . . . . . . . 12
     ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)       ![]](rbrack.gif)
   |
99 | 96, 98 | imbi12d 223 |
. . . . . . . . . . 11
     ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)        ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)        ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      ![]](rbrack.gif)     |
100 | 91, 99 | syl5ibrcom 146 |
. . . . . . . . . 10
     
  
     ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif) 
    |
101 | 100 | impd 242 |
. . . . . . . . 9
     
  
      ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      |
102 | 101 | anassrs 380 |
. . . . . . . 8
   
           ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      |
103 | 102 | rexlimdvva 2434 |
. . . . . . 7
       
     ![]](rbrack.gif)
  ![]](rbrack.gif) 
 
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      |
104 | 61, 103 | syl5bir 142 |
. . . . . 6
            ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      |
105 | 104 | rexlimdvva 2434 |
. . . . 5
          ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)       ![]](rbrack.gif)
  ![]](rbrack.gif)      ![]](rbrack.gif)      |
106 | 60, 105 | syl5bir 142 |
. . . 4
         ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      |
107 | 106 | adantr 261 |
. . 3
             ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      |
108 | 107 | alrimivv 1752 |
. 2
                 ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      |
109 | | eqeq1 2043 |
. . . . 5
 
    ![]](rbrack.gif)     ![]](rbrack.gif)    |
110 | 109 | anbi2d 437 |
. . . 4
      ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)      ![]](rbrack.gif)
  ![]](rbrack.gif)   
  ![]](rbrack.gif)     |
111 | 110 | 2rexbidv 2343 |
. . 3
  

    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)        ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)     |
112 | 111 | eu4 1959 |
. 2
         ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)      
    ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)              ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)   
 
  ![]](rbrack.gif)   ![]](rbrack.gif)   
  ![]](rbrack.gif)       |
113 | 27, 108, 112 | sylanbrc 394 |
1
             ![]](rbrack.gif)   ![]](rbrack.gif) 
 
  ![]](rbrack.gif)    |