Proof of Theorem bj-2upln1upl
Step | Hyp | Ref
| Expression |
1 | | xpundi 4905 |
. . . . . . 7
  
tag
tag       tag    
tag    |
2 | 1 | difeq2i 3559 |
. . . . . 6
    tag    
tag
tag        tag      tag    
tag     |
3 | | incom 3636 |
. . . . . . . . 9
    tag
tag  
   tag
      tag    
tag
tag     |
4 | | bj-disjsn01 31587 |
. . . . . . . . . 10
  
    |
5 | | xpdisj1 5276 |
. . . . . . . . . 10
           tag tag      tag     |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
    tag
tag  
   tag
   |
7 | 3, 6 | eqtr3i 2485 |
. . . . . . . 8
    tag    
tag
tag     |
8 | | disjdif2 3857 |
. . . . . . . 8
     tag     tag
tag        tag     tag tag       tag    |
9 | 7, 8 | ax-mp 5 |
. . . . . . 7
    tag    
tag
tag       tag   |
10 | | bj-1ex 31588 |
. . . . . . . . . 10
 |
11 | 10 | snnz 4102 |
. . . . . . . . 9
   |
12 | | bj-tagn0 31617 |
. . . . . . . . 9
tag  |
13 | 11, 12 | pm3.2i 461 |
. . . . . . . 8
   tag   |
14 | | xpnz 5274 |
. . . . . . . 8
    tag

   tag
   |
15 | 13, 14 | mpbi 213 |
. . . . . . 7
   tag   |
16 | 9, 15 | eqnetri 2705 |
. . . . . 6
    tag    
tag
tag     |
17 | 2, 16 | eqnetrri 2706 |
. . . . 5
    tag      tag    
tag     |
18 | | 0pss 3813 |
. . . . 5
     tag      tag     tag   
    tag 
    tag    
tag      |
19 | 17, 18 | mpbir 214 |
. . . 4
    tag      tag    
tag     |
20 | | ssun2 3609 |
. . . . . . . 8
  
tag     
tag     tag    |
21 | | sscon 3578 |
. . . . . . . 8
    tag 
    tag    
tag  
    tag 
    tag    
tag        tag     tag     |
22 | 20, 21 | ax-mp 5 |
. . . . . . 7
    tag      tag    
tag        tag     tag    |
23 | | ssun2 3609 |
. . . . . . . 8
   tag 
    tag     tag    |
24 | | ssdif 3579 |
. . . . . . . 8
    tag 
    tag     tag       tag     tag        tag     tag      tag     |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
    tag    
tag  
     tag     tag      tag    |
26 | 22, 25 | sstri 3452 |
. . . . . 6
    tag      tag    
tag         tag     tag      tag    |
27 | | df-bj-2upl 31649 |
. . . . . . . 8
(| , |) (| |)    tag    |
28 | | df-bj-1upl 31636 |
. . . . . . . . 9
(| |)    tag   |
29 | 28 | uneq1i 3595 |
. . . . . . . 8
(| |)    tag      
tag     tag    |
30 | 27, 29 | eqtri 2483 |
. . . . . . 7
(| , |)    
tag     tag    |
31 | 30 | difeq1i 3558 |
. . . . . 6
(| , |)   
tag        tag     tag      tag    |
32 | 26, 31 | sseqtr4i 3476 |
. . . . 5
    tag      tag    
tag    (| , |)   
tag    |
33 | | df-bj-1upl 31636 |
. . . . . 6
(| |)    tag   |
34 | 33 | difeq2i 3559 |
. . . . 5
(| , |)
(| |) (| , |)    tag    |
35 | 32, 34 | sseqtr4i 3476 |
. . . 4
    tag      tag    
tag    (| , |)
(| |) |
36 | | psssstr 3550 |
. . . 4
      tag 
    tag    
tag        tag      tag    
tag    (| , |)
(| |)
(| , |)
(| |)  |
37 | 19, 35, 36 | mp2an 683 |
. . 3
(| , |)
(| |) |
38 | | 0pss 3813 |
. . 3
 (| , |) (| |)
(| , |) (| |)
  |
39 | 37, 38 | mpbi 213 |
. 2
(| , |)
(| |)  |
40 | | difn0 3835 |
. 2
 (| , |) (| |)
(| , |) (| |) |
41 | 39, 40 | ax-mp 5 |
1
(| , |) (| |) |