Detailed syntax breakdown of Definition df-imas
Step | Hyp | Ref
| Expression |
1 | | cimas 14564 |
. 2
s |
2 | | vf |
. . 3
 |
3 | | vr |
. . 3
 |
4 | | cvv 3078 |
. . 3
 |
5 | | vv |
. . . 4
 |
6 | 3 | cv 1369 |
. . . . 5
 |
7 | | cbs 14295 |
. . . . 5
 |
8 | 6, 7 | cfv 5529 |
. . . 4
     |
9 | | cnx 14292 |
. . . . . . . . 9
 |
10 | 9, 7 | cfv 5529 |
. . . . . . . 8
     |
11 | 2 | cv 1369 |
. . . . . . . . 9
 |
12 | 11 | crn 4952 |
. . . . . . . 8
 |
13 | 10, 12 | cop 3994 |
. . . . . . 7
        |
14 | | cplusg 14360 |
. . . . . . . . 9
 |
15 | 9, 14 | cfv 5529 |
. . . . . . . 8
    |
16 | | vp |
. . . . . . . . 9
 |
17 | 5 | cv 1369 |
. . . . . . . . 9
 |
18 | | vq |
. . . . . . . . . 10
 |
19 | 16 | cv 1369 |
. . . . . . . . . . . . . 14
 |
20 | 19, 11 | cfv 5529 |
. . . . . . . . . . . . 13
     |
21 | 18 | cv 1369 |
. . . . . . . . . . . . . 14
 |
22 | 21, 11 | cfv 5529 |
. . . . . . . . . . . . 13
     |
23 | 20, 22 | cop 3994 |
. . . . . . . . . . . 12
            |
24 | 6, 14 | cfv 5529 |
. . . . . . . . . . . . . 14
    |
25 | 19, 21, 24 | co 6203 |
. . . . . . . . . . . . 13
        |
26 | 25, 11 | cfv 5529 |
. . . . . . . . . . . 12
            |
27 | 23, 26 | cop 3994 |
. . . . . . . . . . 11
                          |
28 | 27 | csn 3988 |
. . . . . . . . . 10
                            |
29 | 18, 17, 28 | ciun 4282 |
. . . . . . . . 9

                            |
30 | 16, 17, 29 | ciun 4282 |
. . . . . . . 8

                             |
31 | 15, 30 | cop 3994 |
. . . . . . 7
                    
               |
32 | | cmulr 14361 |
. . . . . . . . 9
 |
33 | 9, 32 | cfv 5529 |
. . . . . . . 8
     |
34 | 6, 32 | cfv 5529 |
. . . . . . . . . . . . . 14
     |
35 | 19, 21, 34 | co 6203 |
. . . . . . . . . . . . 13
         |
36 | 35, 11 | cfv 5529 |
. . . . . . . . . . . 12
             |
37 | 23, 36 | cop 3994 |
. . . . . . . . . . 11
                           |
38 | 37 | csn 3988 |
. . . . . . . . . 10
                             |
39 | 18, 17, 38 | ciun 4282 |
. . . . . . . . 9

                             |
40 | 16, 17, 39 | ciun 4282 |
. . . . . . . 8

                              |
41 | 33, 40 | cop 3994 |
. . . . . . 7
                     
                |
42 | 13, 31, 41 | ctp 3992 |
. . . . . 6
                             
                                    
                 |
43 | | csca 14363 |
. . . . . . . . 9
Scalar |
44 | 9, 43 | cfv 5529 |
. . . . . . . 8
Scalar   |
45 | 6, 43 | cfv 5529 |
. . . . . . . 8
Scalar   |
46 | 44, 45 | cop 3994 |
. . . . . . 7
 Scalar   Scalar    |
47 | | cvsca 14364 |
. . . . . . . . 9
 |
48 | 9, 47 | cfv 5529 |
. . . . . . . 8
     |
49 | | vx |
. . . . . . . . . 10
 |
50 | 45, 7 | cfv 5529 |
. . . . . . . . . 10
   Scalar    |
51 | 22 | csn 3988 |
. . . . . . . . . 10
       |
52 | 6, 47 | cfv 5529 |
. . . . . . . . . . . 12
     |
53 | 19, 21, 52 | co 6203 |
. . . . . . . . . . 11
         |
54 | 53, 11 | cfv 5529 |
. . . . . . . . . 10
             |
55 | 16, 49, 50, 51, 54 | cmpt2 6205 |
. . . . . . . . 9
    Scalar                        |
56 | 18, 17, 55 | ciun 4282 |
. . . . . . . 8

    Scalar                        |
57 | 48, 56 | cop 3994 |
. . . . . . 7
           Scalar                         |
58 | | cip 14365 |
. . . . . . . . 9
 |
59 | 9, 58 | cfv 5529 |
. . . . . . . 8
     |
60 | 6, 58 | cfv 5529 |
. . . . . . . . . . . . 13
     |
61 | 19, 21, 60 | co 6203 |
. . . . . . . . . . . 12
         |
62 | 23, 61 | cop 3994 |
. . . . . . . . . . 11
                       |
63 | 62 | csn 3988 |
. . . . . . . . . 10
                         |
64 | 18, 17, 63 | ciun 4282 |
. . . . . . . . 9

                         |
65 | 16, 17, 64 | ciun 4282 |
. . . . . . . 8

                          |
66 | 59, 65 | cop 3994 |
. . . . . . 7
                     
            |
67 | 46, 57, 66 | ctp 3992 |
. . . . . 6
  Scalar   Scalar               Scalar                                              
             |
68 | 42, 67 | cun 3437 |
. . . . 5
       
      
                                                    
                  Scalar   Scalar               Scalar                                              
              |
69 | | cts 14366 |
. . . . . . . 8
TopSet |
70 | 9, 69 | cfv 5529 |
. . . . . . 7
TopSet   |
71 | | ctopn 14482 |
. . . . . . . . 9
 |
72 | 6, 71 | cfv 5529 |
. . . . . . . 8
     |
73 | | cqtop 14563 |
. . . . . . . 8
qTop |
74 | 72, 11, 73 | co 6203 |
. . . . . . 7
     qTop   |
75 | 70, 74 | cop 3994 |
. . . . . 6
 TopSet        qTop    |
76 | | cple 14367 |
. . . . . . . 8
 |
77 | 9, 76 | cfv 5529 |
. . . . . . 7
     |
78 | 6, 76 | cfv 5529 |
. . . . . . . . 9
     |
79 | 11, 78 | ccom 4955 |
. . . . . . . 8
       |
80 | 11 | ccnv 4950 |
. . . . . . . 8
  |
81 | 79, 80 | ccom 4955 |
. . . . . . 7
          |
82 | 77, 81 | cop 3994 |
. . . . . 6
                 |
83 | | cds 14369 |
. . . . . . . 8
 |
84 | 9, 83 | cfv 5529 |
. . . . . . 7
     |
85 | | vy |
. . . . . . . 8
 |
86 | | vn |
. . . . . . . . . 10
 |
87 | | cn 10436 |
. . . . . . . . . 10
 |
88 | | vg |
. . . . . . . . . . . 12
 |
89 | | c1 9397 |
. . . . . . . . . . . . . . . . . 18
 |
90 | | vh |
. . . . . . . . . . . . . . . . . . 19
 |
91 | 90 | cv 1369 |
. . . . . . . . . . . . . . . . . 18
 |
92 | 89, 91 | cfv 5529 |
. . . . . . . . . . . . . . . . 17
     |
93 | | c1st 6688 |
. . . . . . . . . . . . . . . . 17
 |
94 | 92, 93 | cfv 5529 |
. . . . . . . . . . . . . . . 16
         |
95 | 94, 11 | cfv 5529 |
. . . . . . . . . . . . . . 15
             |
96 | 49 | cv 1369 |
. . . . . . . . . . . . . . 15
 |
97 | 95, 96 | wceq 1370 |
. . . . . . . . . . . . . 14
             |
98 | 86 | cv 1369 |
. . . . . . . . . . . . . . . . . 18
 |
99 | 98, 91 | cfv 5529 |
. . . . . . . . . . . . . . . . 17
     |
100 | | c2nd 6689 |
. . . . . . . . . . . . . . . . 17
 |
101 | 99, 100 | cfv 5529 |
. . . . . . . . . . . . . . . 16
         |
102 | 101, 11 | cfv 5529 |
. . . . . . . . . . . . . . 15
             |
103 | 85 | cv 1369 |
. . . . . . . . . . . . . . 15
 |
104 | 102, 103 | wceq 1370 |
. . . . . . . . . . . . . 14
             |
105 | | vi |
. . . . . . . . . . . . . . . . . . . 20
 |
106 | 105 | cv 1369 |
. . . . . . . . . . . . . . . . . . 19
 |
107 | 106, 91 | cfv 5529 |
. . . . . . . . . . . . . . . . . 18
     |
108 | 107, 100 | cfv 5529 |
. . . . . . . . . . . . . . . . 17
         |
109 | 108, 11 | cfv 5529 |
. . . . . . . . . . . . . . . 16
             |
110 | | caddc 9399 |
. . . . . . . . . . . . . . . . . . . 20
 |
111 | 106, 89, 110 | co 6203 |
. . . . . . . . . . . . . . . . . . 19
   |
112 | 111, 91 | cfv 5529 |
. . . . . . . . . . . . . . . . . 18
       |
113 | 112, 93 | cfv 5529 |
. . . . . . . . . . . . . . . . 17
           |
114 | 113, 11 | cfv 5529 |
. . . . . . . . . . . . . . . 16
               |
115 | 109, 114 | wceq 1370 |
. . . . . . . . . . . . . . 15
                           |
116 | | cmin 9709 |
. . . . . . . . . . . . . . . . 17
 |
117 | 98, 89, 116 | co 6203 |
. . . . . . . . . . . . . . . 16
   |
118 | | cfz 11557 |
. . . . . . . . . . . . . . . 16
 |
119 | 89, 117, 118 | co 6203 |
. . . . . . . . . . . . . . 15
       |
120 | 115, 105,
119 | wral 2799 |
. . . . . . . . . . . . . 14
                                   |
121 | 97, 104, 120 | w3a 965 |
. . . . . . . . . . . . 13
                                                             |
122 | 17, 17 | cxp 4949 |
. . . . . . . . . . . . . 14
   |
123 | 89, 98, 118 | co 6203 |
. . . . . . . . . . . . . 14
     |
124 | | cmap 7327 |
. . . . . . . . . . . . . 14
 |
125 | 122, 123,
124 | co 6203 |
. . . . . . . . . . . . 13
         |
126 | 121, 90, 125 | crab 2803 |
. . . . . . . . . . . 12
                                                                       |
127 | | cxrs 14560 |
. . . . . . . . . . . . 13
  |
128 | 6, 83 | cfv 5529 |
. . . . . . . . . . . . . 14
     |
129 | 88 | cv 1369 |
. . . . . . . . . . . . . 14
 |
130 | 128, 129 | ccom 4955 |
. . . . . . . . . . . . 13
       |
131 | | cgsu 14501 |
. . . . . . . . . . . . 13
g |
132 | 127, 130,
131 | co 6203 |
. . . . . . . . . . . 12
  g         |
133 | 88, 126, 132 | cmpt 4461 |
. . . . . . . . . . 11
                                                                         g          |
134 | 133 | crn 4952 |
. . . . . . . . . 10
                                                                         g          |
135 | 86, 87, 134 | ciun 4282 |
. . . . . . . . 9
                                                                          g          |
136 | | cxr 9531 |
. . . . . . . . 9
 |
137 | | clt 9532 |
. . . . . . . . . 10
 |
138 | 137 | ccnv 4950 |
. . . . . . . . 9
 |
139 | 135, 136,
138 | csup 7804 |
. . . . . . . 8
  
                                   
                                     g            |
140 | 49, 85, 12, 12, 139 | cmpt2 6205 |
. . . . . . 7
                                                                              g             |
141 | 84, 140 | cop 3994 |
. . . . . 6
       
  
                                   
                                     g              |
142 | 75, 82, 141 | ctp 3992 |
. . . . 5
  TopSet        qTop                          
                                                                              g               |
143 | 68, 142 | cun 3437 |
. . . 4
        
      
                                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                |
144 | 5, 8, 143 | csb 3398 |
. . 3
      ![]_ ]_](_urbrack.gif)         
      
                                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                |
145 | 2, 3, 4, 4, 144 | cmpt2 6205 |
. 2
        ![]_ ]_](_urbrack.gif)         
      
                                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                 |
146 | 1, 145 | wceq 1370 |
1
s
        ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                 |