Step | Hyp | Ref
| Expression |
1 | | relxp 4947 |
. . . . . . . . 9
   |
2 | | relss 4927 |
. . . . . . . . 9
     
   |
3 | 1, 2 | mpi 20 |
. . . . . . . 8
     |
4 | 3 | ad2antlr 741 |
. . . . . . 7
  
        |
5 | | df-br 4396 |
. . . . . . . . . 10
  
  
  |
6 | | ssun1 3588 |
. . . . . . . . . . . . 13

    |
7 | | undif1 3833 |
. . . . . . . . . . . . 13
             |
8 | 6, 7 | sseqtr4i 3451 |
. . . . . . . . . . . 12
         |
9 | | simpll 768 |
. . . . . . . . . . . . . 14
  
     
  |
10 | | dmss 5039 |
. . . . . . . . . . . . . . . . 17
  
    |
11 | | dmxpid 5060 |
. . . . . . . . . . . . . . . . 17
   |
12 | 10, 11 | syl6sseq 3464 |
. . . . . . . . . . . . . . . 16
     |
13 | 12 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
  
     
  |
14 | 3 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
  
     
  |
15 | | releldm 5073 |
. . . . . . . . . . . . . . . 16
    
  |
16 | 14, 15 | sylancom 680 |
. . . . . . . . . . . . . . 15
  
     
  |
17 | 13, 16 | sseldd 3419 |
. . . . . . . . . . . . . 14
  
     
  |
18 | | sossfld 5289 |
. . . . . . . . . . . . . 14
 
         |
19 | 9, 17, 18 | syl2anc 673 |
. . . . . . . . . . . . 13
  
     
        |
20 | | ssun1 3588 |
. . . . . . . . . . . . . . 15
   |
21 | 20, 16 | sseldi 3416 |
. . . . . . . . . . . . . 14
  
     
    |
22 | 21 | snssd 4108 |
. . . . . . . . . . . . 13
  
     
      |
23 | 19, 22 | unssd 3601 |
. . . . . . . . . . . 12
  
     
            |
24 | 8, 23 | syl5ss 3429 |
. . . . . . . . . . 11
  
     
    |
25 | 24 | ex 441 |
. . . . . . . . . 10
             |
26 | 5, 25 | syl5bir 226 |
. . . . . . . . 9
              |
27 | 26 | con3dimp 448 |
. . . . . . . 8
  
           |
28 | 27 | pm2.21d 109 |
. . . . . . 7
  
         
      |
29 | 4, 28 | relssdv 4932 |
. . . . . 6
  
        |
30 | | ss0 3768 |
. . . . . 6

  |
31 | 29, 30 | syl 17 |
. . . . 5
  
        |
32 | 31 | ex 441 |
. . . 4
       
   |
33 | 32 | necon1ad 2660 |
. . 3
           |
34 | 33 | 3impia 1228 |
. 2
         |
35 | | rnss 5069 |
. . . . 5
  
    |
36 | | rnxpid 5276 |
. . . . 5
   |
37 | 35, 36 | syl6sseq 3464 |
. . . 4
     |
38 | 12, 37 | unssd 3601 |
. . 3
    
  |
39 | 38 | 3ad2ant2 1052 |
. 2
      
  |
40 | 34, 39 | eqssd 3435 |
1
         |