Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-imas Unicode version

Definition df-imas 13411
 Description: Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly must either be injective or satisfy the well-definedness condition for each relevant operation. Note that although we call this an "image" by association to df-ima 4702, in order to keep the definition simple we consider only the case when the domain of is equal to the base set of . Other cases can be achieved by restricting (with df-res 4701) and/or ( with df-ress 13155) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.)
Assertion
Ref Expression
df-imas s Scalar Scalar Scalar TopSet qTop g
Distinct variable group:   ,,,,,,,,,,

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 13407 . 2 s
2 vf . . 3
3 vr . . 3
4 cvv 2788 . . 3
5 vv . . . 4
63cv 1622 . . . . 5
7 cbs 13148 . . . . 5
86, 7cfv 5255 . . . 4
9 cnx 13145 . . . . . . . . 9
109, 7cfv 5255 . . . . . . . 8
112cv 1622 . . . . . . . . 9
1211crn 4690 . . . . . . . 8
1310, 12cop 3643 . . . . . . 7
14 cplusg 13208 . . . . . . . . 9
159, 14cfv 5255 . . . . . . . 8
16 vp . . . . . . . . 9
175cv 1622 . . . . . . . . 9
18 vq . . . . . . . . . 10
1916cv 1622 . . . . . . . . . . . . . 14
2019, 11cfv 5255 . . . . . . . . . . . . 13
2118cv 1622 . . . . . . . . . . . . . 14
2221, 11cfv 5255 . . . . . . . . . . . . 13
2320, 22cop 3643 . . . . . . . . . . . 12
246, 14cfv 5255 . . . . . . . . . . . . . 14
2519, 21, 24co 5858 . . . . . . . . . . . . 13
2625, 11cfv 5255 . . . . . . . . . . . 12
2723, 26cop 3643 . . . . . . . . . . 11
2827csn 3640 . . . . . . . . . 10
2918, 17, 28ciun 3905 . . . . . . . . 9
3016, 17, 29ciun 3905 . . . . . . . 8
3115, 30cop 3643 . . . . . . 7
32 cmulr 13209 . . . . . . . . 9
339, 32cfv 5255 . . . . . . . 8
346, 32cfv 5255 . . . . . . . . . . . . . 14
3519, 21, 34co 5858 . . . . . . . . . . . . 13
3635, 11cfv 5255 . . . . . . . . . . . 12
3723, 36cop 3643 . . . . . . . . . . 11
3837csn 3640 . . . . . . . . . 10
3918, 17, 38ciun 3905 . . . . . . . . 9
4016, 17, 39ciun 3905 . . . . . . . 8
4133, 40cop 3643 . . . . . . 7
4213, 31, 41ctp 3642 . . . . . 6
43 csca 13211 . . . . . . . . 9 Scalar
449, 43cfv 5255 . . . . . . . 8 Scalar
456, 43cfv 5255 . . . . . . . 8 Scalar
4644, 45cop 3643 . . . . . . 7 Scalar Scalar
47 cvsca 13212 . . . . . . . . 9
489, 47cfv 5255 . . . . . . . 8
49 vx . . . . . . . . . 10
5045, 7cfv 5255 . . . . . . . . . 10 Scalar
5122csn 3640 . . . . . . . . . 10
526, 47cfv 5255 . . . . . . . . . . . 12
5319, 21, 52co 5858 . . . . . . . . . . 11
5453, 11cfv 5255 . . . . . . . . . 10
5516, 49, 50, 51, 54cmpt2 5860 . . . . . . . . 9 Scalar
5618, 17, 55ciun 3905 . . . . . . . 8 Scalar
5748, 56cop 3643 . . . . . . 7 Scalar
5846, 57cpr 3641 . . . . . 6 Scalar Scalar Scalar
5942, 58cun 3150 . . . . 5 Scalar Scalar Scalar
60 cts 13214 . . . . . . . 8 TopSet
619, 60cfv 5255 . . . . . . 7 TopSet
62 ctopn 13326 . . . . . . . . 9
636, 62cfv 5255 . . . . . . . 8
64 cqtop 13406 . . . . . . . 8 qTop
6563, 11, 64co 5858 . . . . . . 7 qTop
6661, 65cop 3643 . . . . . 6 TopSet qTop
67 cple 13215 . . . . . . . 8
689, 67cfv 5255 . . . . . . 7
696, 67cfv 5255 . . . . . . . . 9
7011, 69ccom 4693 . . . . . . . 8
7111ccnv 4688 . . . . . . . 8
7270, 71ccom 4693 . . . . . . 7
7368, 72cop 3643 . . . . . 6
74 cds 13217 . . . . . . . 8
759, 74cfv 5255 . . . . . . 7
76 vy . . . . . . . 8
77 vn . . . . . . . . . 10
78 cn 9746 . . . . . . . . . 10
79 vg . . . . . . . . . . . 12
80 c1 8738 . . . . . . . . . . . . . . . . . 18
81 vh . . . . . . . . . . . . . . . . . . 19
8281cv 1622 . . . . . . . . . . . . . . . . . 18
8380, 82cfv 5255 . . . . . . . . . . . . . . . . 17
84 c1st 6120 . . . . . . . . . . . . . . . . 17
8583, 84cfv 5255 . . . . . . . . . . . . . . . 16
8685, 11cfv 5255 . . . . . . . . . . . . . . 15
8749cv 1622 . . . . . . . . . . . . . . 15
8886, 87wceq 1623 . . . . . . . . . . . . . 14
8977cv 1622 . . . . . . . . . . . . . . . . . 18
9089, 82cfv 5255 . . . . . . . . . . . . . . . . 17
91 c2nd 6121 . . . . . . . . . . . . . . . . 17
9290, 91cfv 5255 . . . . . . . . . . . . . . . 16
9392, 11cfv 5255 . . . . . . . . . . . . . . 15
9476cv 1622 . . . . . . . . . . . . . . 15
9593, 94wceq 1623 . . . . . . . . . . . . . 14
96 vi . . . . . . . . . . . . . . . . . . . 20
9796cv 1622 . . . . . . . . . . . . . . . . . . 19
9897, 82cfv 5255 . . . . . . . . . . . . . . . . . 18
9998, 91cfv 5255 . . . . . . . . . . . . . . . . 17
10099, 11cfv 5255 . . . . . . . . . . . . . . . 16
101 caddc 8740 . . . . . . . . . . . . . . . . . . . 20
10297, 80, 101co 5858 . . . . . . . . . . . . . . . . . . 19
103102, 82cfv 5255 . . . . . . . . . . . . . . . . . 18
104103, 84cfv 5255 . . . . . . . . . . . . . . . . 17
105104, 11cfv 5255 . . . . . . . . . . . . . . . 16
106100, 105wceq 1623 . . . . . . . . . . . . . . 15
107 cmin 9037 . . . . . . . . . . . . . . . . 17
10889, 80, 107co 5858 . . . . . . . . . . . . . . . 16
109 cfz 10782 . . . . . . . . . . . . . . . 16
11080, 108, 109co 5858 . . . . . . . . . . . . . . 15
111106, 96, 110wral 2543 . . . . . . . . . . . . . 14
11288, 95, 111w3a 934 . . . . . . . . . . . . 13
11317, 17cxp 4687 . . . . . . . . . . . . . 14
11480, 89, 109co 5858 . . . . . . . . . . . . . 14
115 cmap 6772 . . . . . . . . . . . . . 14
116113, 114, 115co 5858 . . . . . . . . . . . . 13
117112, 81, 116crab 2547 . . . . . . . . . . . 12
118 cxrs 13399 . . . . . . . . . . . . 13
1196, 74cfv 5255 . . . . . . . . . . . . . 14
12079cv 1622 . . . . . . . . . . . . . 14
121119, 120ccom 4693 . . . . . . . . . . . . 13
122 cgsu 13401 . . . . . . . . . . . . 13 g
123118, 121, 122co 5858 . . . . . . . . . . . 12 g
12479, 117, 123cmpt 4077 . . . . . . . . . . 11 g
125124crn 4690 . . . . . . . . . 10 g
12677, 78, 125ciun 3905 . . . . . . . . 9 g
127 cxr 8866 . . . . . . . . 9
128 clt 8867 . . . . . . . . . 10
129128ccnv 4688 . . . . . . . . 9
130126, 127, 129csup 7193 . . . . . . . 8 g
13149, 76, 12, 12, 130cmpt2 5860 . . . . . . 7 g
13275, 131cop 3643 . . . . . 6 g
13366, 73, 132ctp 3642 . . . . 5 TopSet qTop g
13459, 133cun 3150 . . . 4 Scalar Scalar Scalar TopSet qTop g
1355, 8, 134csb 3081 . . 3 Scalar Scalar Scalar TopSet qTop g
1362, 3, 4, 4, 135cmpt2 5860 . 2 Scalar Scalar Scalar TopSet qTop g
1371, 136wceq 1623 1 s Scalar Scalar Scalar TopSet qTop g
 Colors of variables: wff set class This definition is referenced by:  imasval  13414
 Copyright terms: Public domain W3C validator