Step | Hyp | Ref
| Expression |
1 | | df-on 5445 |
. 2

  |
2 | | tz7.7 5467 |
. . . . . . . . 9
   
     |
3 | | df-pss 3431 |
. . . . . . . . 9

    |
4 | 2, 3 | syl6bbr 271 |
. . . . . . . 8
   
   |
5 | 4 | exbiri 632 |
. . . . . . 7

      |
6 | 5 | com23 81 |
. . . . . 6


     |
7 | 6 | impd 437 |
. . . . 5

 
    |
8 | 7 | alrimiv 1783 |
. . . 4

        |
9 | | vex 3059 |
. . . . . . 7
 |
10 | | dfon2lem3 30479 |
. . . . . . 7
        

    |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
       

   |
12 | 11 | simpld 465 |
. . . . 5
         |
13 | 9 | dfon2lem7 30483 |
. . . . . . . 8
                 |
14 | 13 | ralrimiv 2811 |
. . . . . . 7
       
        |
15 | | dfon2lem9 30485 |
. . . . . . . 8
 
        |
16 | | psseq2 3532 |
. . . . . . . . . . . . . . . 16
 
   |
17 | 16 | anbi1d 716 |
. . . . . . . . . . . . . . 15
   
     |
18 | | elequ2 1911 |
. . . . . . . . . . . . . . 15
 
   |
19 | 17, 18 | imbi12d 326 |
. . . . . . . . . . . . . 14
             |
20 | 19 | albidv 1777 |
. . . . . . . . . . . . 13
       
         |
21 | | psseq1 3531 |
. . . . . . . . . . . . . . . 16
 
   |
22 | | treq 4516 |
. . . . . . . . . . . . . . . 16
 
   |
23 | 21, 22 | anbi12d 722 |
. . . . . . . . . . . . . . 15
   
     |
24 | | elequ1 1904 |
. . . . . . . . . . . . . . 15
 
   |
25 | 23, 24 | imbi12d 326 |
. . . . . . . . . . . . . 14
             |
26 | 25 | cbvalv 2126 |
. . . . . . . . . . . . 13
      
        |
27 | 20, 26 | syl6bb 269 |
. . . . . . . . . . . 12
       
         |
28 | 27 | rspccv 3158 |
. . . . . . . . . . 11
 
                |
29 | | psseq2 3532 |
. . . . . . . . . . . . . . . 16
 
   |
30 | 29 | anbi1d 716 |
. . . . . . . . . . . . . . 15
   
     |
31 | | elequ2 1911 |
. . . . . . . . . . . . . . 15
 
   |
32 | 30, 31 | imbi12d 326 |
. . . . . . . . . . . . . 14
             |
33 | 32 | albidv 1777 |
. . . . . . . . . . . . 13
       
         |
34 | | psseq1 3531 |
. . . . . . . . . . . . . . . 16
 
   |
35 | | treq 4516 |
. . . . . . . . . . . . . . . 16
 
   |
36 | 34, 35 | anbi12d 722 |
. . . . . . . . . . . . . . 15
   
     |
37 | | elequ1 1904 |
. . . . . . . . . . . . . . 15
 
   |
38 | 36, 37 | imbi12d 326 |
. . . . . . . . . . . . . 14
             |
39 | 38 | cbvalv 2126 |
. . . . . . . . . . . . 13
      
        |
40 | 33, 39 | syl6bb 269 |
. . . . . . . . . . . 12
       
         |
41 | 40 | rspccv 3158 |
. . . . . . . . . . 11
 
                |
42 | 28, 41 | anim12d 570 |
. . . . . . . . . 10
 
       

                 |
43 | | vex 3059 |
. . . . . . . . . . 11
 |
44 | | vex 3059 |
. . . . . . . . . . 11
 |
45 | 43, 44 | dfon2lem5 30481 |
. . . . . . . . . 10
     
         
   |
46 | 42, 45 | syl6 34 |
. . . . . . . . 9
 
       


    |
47 | 46 | ralrimivv 2819 |
. . . . . . . 8
 
      


   |
48 | 15, 47 | jca 539 |
. . . . . . 7
 
      

     |
49 | 14, 48 | syl 17 |
. . . . . 6
       

     |
50 | | dfwe2 6634 |
. . . . . . 7



    |
51 | | epel 4766 |
. . . . . . . . . 10

  |
52 | | biid 244 |
. . . . . . . . . 10

  |
53 | | epel 4766 |
. . . . . . . . . 10

  |
54 | 51, 52, 53 | 3orbi123i 1204 |
. . . . . . . . 9
   
   |
55 | 54 | 2ralbii 2831 |
. . . . . . . 8
 

  


   |
56 | 55 | anbi2i 705 |
. . . . . . 7
  
          |
57 | 50, 56 | bitri 257 |
. . . . . 6



    |
58 | 49, 57 | sylibr 217 |
. . . . 5
         |
59 | | df-ord 5444 |
. . . . 5
     |
60 | 12, 58, 59 | sylanbrc 675 |
. . . 4
         |
61 | 8, 60 | impbii 192 |
. . 3
    
    |
62 | 61 | abbii 2577 |
. 2
  
        |
63 | 1, 62 | eqtri 2483 |
1

        |