Proof of Theorem mdsymlem3
Step | Hyp | Ref
| Expression |
1 | | atelch 25920 |
. . . . . 6
 HAtoms   |
2 | | mdsymlem1.2 |
. . . . . . 7
 |
3 | | mdsymlem1.3 |
. . . . . . . 8
   |
4 | | mdsymlem1.1 |
. . . . . . . . 9
 |
5 | | chjcl 24932 |
. . . . . . . . 9
 
     |
6 | 4, 5 | mpan 670 |
. . . . . . . 8
     |
7 | 3, 6 | syl5eqel 2546 |
. . . . . . 7
   |
8 | | chincl 25074 |
. . . . . . 7
 
     |
9 | 2, 7, 8 | sylancr 663 |
. . . . . 6
     |
10 | 1, 9 | syl 16 |
. . . . 5
 HAtoms     |
11 | | chrelat2 25946 |
. . . . 5
   
     HAtoms 
      |
12 | 10, 4, 11 | sylancl 662 |
. . . 4
 HAtoms     HAtoms 
      |
13 | 12 | biimpa 484 |
. . 3
  HAtoms
    HAtoms   
   |
14 | 13 | ad2antrr 725 |
. 2
    HAtoms  

     HAtoms 
     |
15 | | ssin 3683 |
. . . . . . . . . . . 12
 


   |
16 | 3 | sseq2i 3492 |
. . . . . . . . . . . . . 14


   |
17 | 16 | biimpi 194 |
. . . . . . . . . . . . 13
     |
18 | 17 | adantl 466 |
. . . . . . . . . . . 12
 

    |
19 | 15, 18 | sylbir 213 |
. . . . . . . . . . 11
  

   |
20 | 4 | atcvat4i 25973 |
. . . . . . . . . . . . . . 15
  HAtoms
HAtoms
      HAtoms 
      |
21 | 20 | exp4b 607 |
. . . . . . . . . . . . . 14
 HAtoms  HAtoms     
HAtoms          |
22 | 21 | com34 83 |
. . . . . . . . . . . . 13
 HAtoms  HAtoms      HAtoms 
        |
23 | 22 | com23 78 |
. . . . . . . . . . . 12
 HAtoms  

 HAtoms   HAtoms 
        |
24 | 23 | imp4b 590 |
. . . . . . . . . . 11
  HAtoms
     HAtoms   HAtoms 
      |
25 | 19, 24 | sylan2 474 |
. . . . . . . . . 10
  HAtoms
     HAtoms   HAtoms 
      |
26 | 25 | adantrr 716 |
. . . . . . . . 9
  HAtoms

      HAtoms   HAtoms 
      |
27 | 26 | com12 31 |
. . . . . . . 8
  HAtoms
   HAtoms 
     HAtoms 
      |
28 | 27 | adantlr 714 |
. . . . . . 7
   HAtoms 
     HAtoms   
 
 HAtoms 
      |
29 | 28 | adantlr 714 |
. . . . . 6
    HAtoms  

      HAtoms  
   
HAtoms        |
30 | 29 | imp 429 |
. . . . 5
     HAtoms         HAtoms

    
 HAtoms 
     |
31 | | nssne2 3524 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
32 | 31 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
 
  |
33 | | atnemeq0 25953 |
. . . . . . . . . . . . . . . . . . . . . . 23
  HAtoms
HAtoms

     |
34 | 33 | ancoms 453 |
. . . . . . . . . . . . . . . . . . . . . 22
  HAtoms
HAtoms

     |
35 | 32, 34 | syl5ib 219 |
. . . . . . . . . . . . . . . . . . . . 21
  HAtoms
HAtoms
 
  
 
     |
36 | 35 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
   HAtoms HAtoms HAtoms
 
  
 
     |
37 | 36 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
    HAtoms
HAtoms
HAtoms        
 
     |
38 | | atelch 25920 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 HAtoms   |
39 | | chjcom 25081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
40 | 1, 38, 39 | syl2an 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
  HAtoms
HAtoms
      |
41 | 40 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . 22
   HAtoms HAtoms HAtoms
      |
42 | 41 | sseq2d 3495 |
. . . . . . . . . . . . . . . . . . . . 21
   HAtoms HAtoms HAtoms
   
    |
43 | | atexch 25957 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
HAtoms HAtoms
 
  
       |
44 | 38, 43 | syl3an1 1252 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  HAtoms
HAtoms HAtoms    
  

    |
45 | 44 | 3com13 1193 |
. . . . . . . . . . . . . . . . . . . . . . 23
  HAtoms
HAtoms HAtoms    
  

    |
46 | 45 | 3expa 1188 |
. . . . . . . . . . . . . . . . . . . . . 22
   HAtoms HAtoms HAtoms
 
  
       |
47 | 46 | expd 436 |
. . . . . . . . . . . . . . . . . . . . 21
   HAtoms HAtoms HAtoms
  
 

      |
48 | 42, 47 | sylbid 215 |
. . . . . . . . . . . . . . . . . . . 20
   HAtoms HAtoms HAtoms
  
 

      |
49 | 48 | imp 429 |
. . . . . . . . . . . . . . . . . . 19
    HAtoms
HAtoms
HAtoms            |
50 | 37, 49 | syld 44 |
. . . . . . . . . . . . . . . . . 18
    HAtoms
HAtoms
HAtoms        
 

    |
51 | 50 | expd 436 |
. . . . . . . . . . . . . . . . 17
    HAtoms
HAtoms
HAtoms    
   
 
     |
52 | 51 | exp31 604 |
. . . . . . . . . . . . . . . 16
  HAtoms
HAtoms
 HAtoms  


 
           |
53 | 52 | com24 87 |
. . . . . . . . . . . . . . 15
  HAtoms
HAtoms

  
 HAtoms              |
54 | 53 | impd 431 |
. . . . . . . . . . . . . 14
  HAtoms
HAtoms
 
    HAtoms    
 
      |
55 | 54 | com24 87 |
. . . . . . . . . . . . 13
  HAtoms
HAtoms
 
    HAtoms  
   
      |
56 | 55 | imp4b 590 |
. . . . . . . . . . . 12
   HAtoms HAtoms        HAtoms 
   

    |
57 | 56 | anasss 647 |
. . . . . . . . . . 11
  HAtoms
 HAtoms

    
  HAtoms

    
    |
58 | | simprl 755 |
. . . . . . . . . . . . 13
  HAtoms

      |
59 | 58 | a1i 11 |
. . . . . . . . . . . 12
  HAtoms
 HAtoms

    
  HAtoms

       |
60 | | simpl 457 |
. . . . . . . . . . . . . . 15
 

  |
61 | 15, 60 | sylbir 213 |
. . . . . . . . . . . . . 14
  
  |
62 | 61 | ad2antrl 727 |
. . . . . . . . . . . . 13
  HAtoms

      |
63 | 62 | adantl 466 |
. . . . . . . . . . . 12
  HAtoms
 HAtoms

    
  |
64 | 59, 63 | jctird 544 |
. . . . . . . . . . 11
  HAtoms
 HAtoms

    
  HAtoms

         |
65 | 57, 64 | jcad 533 |
. . . . . . . . . 10
  HAtoms
 HAtoms

    
  HAtoms

      
      |
66 | 65 | expd 436 |
. . . . . . . . 9
  HAtoms
 HAtoms

    
 HAtoms      
  
      |
67 | 66 | adantlr 714 |
. . . . . . . 8
   HAtoms 
   HAtoms 
    
 HAtoms      
  
      |
68 | 67 | adantlr 714 |
. . . . . . 7
    HAtoms  

    HAtoms   
    HAtoms
 
    
 
      |
69 | 68 | adantlr 714 |
. . . . . 6
     HAtoms         HAtoms

    
 HAtoms      
  
      |
70 | 69 | reximdvai 2932 |
. . . . 5
     HAtoms         HAtoms

    
 
HAtoms  
   HAtoms  
 
     |
71 | 30, 70 | mpd 15 |
. . . 4
     HAtoms         HAtoms

    
 HAtoms  
 
    |
72 | 71 | exp32 605 |
. . 3
    HAtoms  

     HAtoms   
   HAtoms  
 
      |
73 | 72 | reximdvai 2932 |
. 2
    HAtoms  

      HAtoms   
  HAtoms  HAtoms  
 
     |
74 | 14, 73 | mpd 15 |
1
    HAtoms  

     HAtoms  HAtoms  
 
    |