Step | Hyp | Ref
| Expression |
1 | | reltpos 6975 |
. 2
tpos tpos  |
2 | | inss2 3652 |
. . 3
                   |
3 | | relxp 4941 |
. . 3
   
     |
4 | | relss 4921 |
. . 3
     
                     
             |
5 | 2, 3, 4 | mp2 9 |
. 2
           |
6 | | relcnv 5206 |
. . . . . . . . 9
 tpos  |
7 | | df-rel 4840 |
. . . . . . . . 9
  tpos
 tpos
    |
8 | 6, 7 | mpbi 212 |
. . . . . . . 8
 tpos    |
9 | | simpl 459 |
. . . . . . . 8
   tpos     tpos
 
 tpos   |
10 | 8, 9 | sseldi 3429 |
. . . . . . 7
   tpos     tpos
 

   |
11 | | simpr 463 |
. . . . . . 7
   
  
    |
12 | | elvv 4892 |
. . . . . . . . 9
  
  
     |
13 | | eleq1 2516 |
. . . . . . . . . . . . . 14
      tpos
    tpos    |
14 | | vex 3047 |
. . . . . . . . . . . . . . 15
 |
15 | | vex 3047 |
. . . . . . . . . . . . . . 15
 |
16 | 14, 15 | opelcnv 5015 |
. . . . . . . . . . . . . 14
     tpos
   tpos
  |
17 | 13, 16 | syl6bb 265 |
. . . . . . . . . . . . 13
      tpos
   tpos
   |
18 | | sneq 3977 |
. . . . . . . . . . . . . . . . 17
             |
19 | 18 | cnveqd 5009 |
. . . . . . . . . . . . . . . 16
      
        |
20 | 19 | unieqd 4207 |
. . . . . . . . . . . . . . 15
       
         |
21 | | opswap 5322 |
. . . . . . . . . . . . . . 15
           |
22 | 20, 21 | syl6eq 2500 |
. . . . . . . . . . . . . 14
       
     |
23 | 22 | breq1d 4411 |
. . . . . . . . . . . . 13
         tpos     tpos     |
24 | 17, 23 | anbi12d 716 |
. . . . . . . . . . . 12
       tpos     tpos  
    tpos    tpos      |
25 | | opex 4663 |
. . . . . . . . . . . . . . 15
  
 |
26 | | vex 3047 |
. . . . . . . . . . . . . . 15
 |
27 | 25, 26 | breldm 5038 |
. . . . . . . . . . . . . 14
    tpos 
  
tpos   |
28 | 27 | pm4.71ri 638 |
. . . . . . . . . . . . 13
    tpos     
tpos    tpos     |
29 | | brtpos 6979 |
. . . . . . . . . . . . . 14
     tpos          |
30 | 26, 29 | ax-mp 5 |
. . . . . . . . . . . . 13
    tpos         |
31 | 28, 30 | bitr3i 255 |
. . . . . . . . . . . 12
     tpos    tpos  
       |
32 | 24, 31 | syl6bb 265 |
. . . . . . . . . . 11
       tpos     tpos  
        |
33 | | breq1 4404 |
. . . . . . . . . . 11
               |
34 | 32, 33 | bitr4d 260 |
. . . . . . . . . 10
       tpos     tpos  
     |
35 | 34 | exlimivv 1777 |
. . . . . . . . 9
          tpos     tpos  
     |
36 | 12, 35 | sylbi 199 |
. . . . . . . 8
  
   tpos     tpos
       |
37 | | iba 506 |
. . . . . . . 8
  
  
         |
38 | 36, 37 | bitrd 257 |
. . . . . . 7
  
   tpos     tpos
           |
39 | 10, 11, 38 | pm5.21nii 355 |
. . . . . 6
   tpos     tpos
          |
40 | | elsni 3992 |
. . . . . . . . . . . . . . . 16
     |
41 | 40 | sneqd 3979 |
. . . . . . . . . . . . . . 15
         |
42 | 41 | cnveqd 5009 |
. . . . . . . . . . . . . 14
           |
43 | | cnvsn0 5303 |
. . . . . . . . . . . . . 14
    |
44 | 42, 43 | syl6eq 2500 |
. . . . . . . . . . . . 13
        |
45 | 44 | unieqd 4207 |
. . . . . . . . . . . 12
          |
46 | | uni0 4224 |
. . . . . . . . . . . 12
  |
47 | 45, 46 | syl6eq 2500 |
. . . . . . . . . . 11
         |
48 | 47 | breq1d 4411 |
. . . . . . . . . 10
        tpos 
tpos     |
49 | | brtpos0 6977 |
. . . . . . . . . . 11
  tpos 
     |
50 | 26, 49 | ax-mp 5 |
. . . . . . . . . 10
 tpos      |
51 | 48, 50 | syl6bb 265 |
. . . . . . . . 9
        tpos 
     |
52 | 40 | breq1d 4411 |
. . . . . . . . 9
     
     |
53 | 51, 52 | bitr4d 260 |
. . . . . . . 8
        tpos 
     |
54 | 53 | pm5.32i 642 |
. . . . . . 7
        tpos
          |
55 | | ancom 452 |
. . . . . . 7
               |
56 | 54, 55 | bitri 253 |
. . . . . 6
        tpos
          |
57 | 39, 56 | orbi12i 524 |
. . . . 5
    tpos     tpos          tpos
  
   
            |
58 | | andir 878 |
. . . . 5
    tpos        tpos  
   tpos     tpos
         tpos      |
59 | | andi 877 |
. . . . 5
    
     
   
            |
60 | 57, 58, 59 | 3bitr4i 281 |
. . . 4
    tpos        tpos  
            |
61 | | elun 3573 |
. . . . 5
   tpos      tpos      |
62 | 61 | anbi1i 700 |
. . . 4
    tpos
       tpos  
   tpos        tpos     |
63 | | brxp 4864 |
. . . . . . 7
          
   
      |
64 | 26, 63 | mpbiran2 929 |
. . . . . 6
          
  
     |
65 | | elun 3573 |
. . . . . 6
      
  
     |
66 | 64, 65 | bitri 253 |
. . . . 5
          
  
     |
67 | 66 | anbi2i 699 |
. . . 4
                    
      |
68 | 60, 62, 67 | 3bitr4i 281 |
. . 3
    tpos
       tpos  
                |
69 | | brtpos2 6976 |
. . . 4
  tpos tpos 
   tpos        tpos      |
70 | 26, 69 | ax-mp 5 |
. . 3
 tpos tpos 
   tpos        tpos     |
71 | | brin 4451 |
. . 3
      
     
                |
72 | 68, 70, 71 | 3bitr4i 281 |
. 2
 tpos tpos 
              |
73 | 1, 5, 72 | eqbrriv 4929 |
1
tpos tpos     
      |