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

Definition df-imas 15485
 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 4852, 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 4851) and/or ( with df-ress 15206) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)
Assertion
Ref Expression
df-imas s Scalar Scalar Scalar TopSet qTop inf g
Distinct variable group:   ,,,,,,,,,,

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 15480 . 2 s
2 vf . . 3
3 vr . . 3
4 cvv 3031 . . 3
5 vv . . . 4
63cv 1451 . . . . 5
7 cbs 15199 . . . . 5
86, 7cfv 5589 . . . 4
9 cnx 15196 . . . . . . . . 9
109, 7cfv 5589 . . . . . . . 8
112cv 1451 . . . . . . . . 9
1211crn 4840 . . . . . . . 8
1310, 12cop 3965 . . . . . . 7
14 cplusg 15268 . . . . . . . . 9
159, 14cfv 5589 . . . . . . . 8
16 vp . . . . . . . . 9
175cv 1451 . . . . . . . . 9
18 vq . . . . . . . . . 10
1916cv 1451 . . . . . . . . . . . . . 14
2019, 11cfv 5589 . . . . . . . . . . . . 13
2118cv 1451 . . . . . . . . . . . . . 14
2221, 11cfv 5589 . . . . . . . . . . . . 13
2320, 22cop 3965 . . . . . . . . . . . 12
246, 14cfv 5589 . . . . . . . . . . . . . 14
2519, 21, 24co 6308 . . . . . . . . . . . . 13
2625, 11cfv 5589 . . . . . . . . . . . 12
2723, 26cop 3965 . . . . . . . . . . 11
2827csn 3959 . . . . . . . . . 10
2918, 17, 28ciun 4269 . . . . . . . . 9
3016, 17, 29ciun 4269 . . . . . . . 8
3115, 30cop 3965 . . . . . . 7
32 cmulr 15269 . . . . . . . . 9
339, 32cfv 5589 . . . . . . . 8
346, 32cfv 5589 . . . . . . . . . . . . . 14
3519, 21, 34co 6308 . . . . . . . . . . . . 13
3635, 11cfv 5589 . . . . . . . . . . . 12
3723, 36cop 3965 . . . . . . . . . . 11
3837csn 3959 . . . . . . . . . 10
3918, 17, 38ciun 4269 . . . . . . . . 9
4016, 17, 39ciun 4269 . . . . . . . 8
4133, 40cop 3965 . . . . . . 7
4213, 31, 41ctp 3963 . . . . . 6
43 csca 15271 . . . . . . . . 9 Scalar
449, 43cfv 5589 . . . . . . . 8 Scalar
456, 43cfv 5589 . . . . . . . 8 Scalar
4644, 45cop 3965 . . . . . . 7 Scalar Scalar
47 cvsca 15272 . . . . . . . . 9
489, 47cfv 5589 . . . . . . . 8
49 vx . . . . . . . . . 10
5045, 7cfv 5589 . . . . . . . . . 10 Scalar
5122csn 3959 . . . . . . . . . 10
526, 47cfv 5589 . . . . . . . . . . . 12
5319, 21, 52co 6308 . . . . . . . . . . 11
5453, 11cfv 5589 . . . . . . . . . 10
5516, 49, 50, 51, 54cmpt2 6310 . . . . . . . . 9 Scalar
5618, 17, 55ciun 4269 . . . . . . . 8 Scalar
5748, 56cop 3965 . . . . . . 7 Scalar
58 cip 15273 . . . . . . . . 9
599, 58cfv 5589 . . . . . . . 8
606, 58cfv 5589 . . . . . . . . . . . . 13
6119, 21, 60co 6308 . . . . . . . . . . . 12
6223, 61cop 3965 . . . . . . . . . . 11
6362csn 3959 . . . . . . . . . 10
6418, 17, 63ciun 4269 . . . . . . . . 9
6516, 17, 64ciun 4269 . . . . . . . 8
6659, 65cop 3965 . . . . . . 7
6746, 57, 66ctp 3963 . . . . . 6 Scalar Scalar Scalar
6842, 67cun 3388 . . . . 5 Scalar Scalar Scalar
69 cts 15274 . . . . . . . 8 TopSet
709, 69cfv 5589 . . . . . . 7 TopSet
71 ctopn 15398 . . . . . . . . 9
726, 71cfv 5589 . . . . . . . 8
73 cqtop 15479 . . . . . . . 8 qTop
7472, 11, 73co 6308 . . . . . . 7 qTop
7570, 74cop 3965 . . . . . 6 TopSet qTop
76 cple 15275 . . . . . . . 8
779, 76cfv 5589 . . . . . . 7
786, 76cfv 5589 . . . . . . . . 9
7911, 78ccom 4843 . . . . . . . 8
8011ccnv 4838 . . . . . . . 8
8179, 80ccom 4843 . . . . . . 7
8277, 81cop 3965 . . . . . 6
83 cds 15277 . . . . . . . 8
849, 83cfv 5589 . . . . . . 7
85 vy . . . . . . . 8
86 vn . . . . . . . . . 10
87 cn 10631 . . . . . . . . . 10
88 vg . . . . . . . . . . . 12
89 c1 9558 . . . . . . . . . . . . . . . . . 18
90 vh . . . . . . . . . . . . . . . . . . 19
9190cv 1451 . . . . . . . . . . . . . . . . . 18
9289, 91cfv 5589 . . . . . . . . . . . . . . . . 17
93 c1st 6810 . . . . . . . . . . . . . . . . 17
9492, 93cfv 5589 . . . . . . . . . . . . . . . 16
9594, 11cfv 5589 . . . . . . . . . . . . . . 15
9649cv 1451 . . . . . . . . . . . . . . 15
9795, 96wceq 1452 . . . . . . . . . . . . . 14
9886cv 1451 . . . . . . . . . . . . . . . . . 18
9998, 91cfv 5589 . . . . . . . . . . . . . . . . 17
100 c2nd 6811 . . . . . . . . . . . . . . . . 17
10199, 100cfv 5589 . . . . . . . . . . . . . . . 16
102101, 11cfv 5589 . . . . . . . . . . . . . . 15
10385cv 1451 . . . . . . . . . . . . . . 15
104102, 103wceq 1452 . . . . . . . . . . . . . 14
105 vi . . . . . . . . . . . . . . . . . . . 20
106105cv 1451 . . . . . . . . . . . . . . . . . . 19
107106, 91cfv 5589 . . . . . . . . . . . . . . . . . 18
108107, 100cfv 5589 . . . . . . . . . . . . . . . . 17
109108, 11cfv 5589 . . . . . . . . . . . . . . . 16
110 caddc 9560 . . . . . . . . . . . . . . . . . . . 20
111106, 89, 110co 6308 . . . . . . . . . . . . . . . . . . 19
112111, 91cfv 5589 . . . . . . . . . . . . . . . . . 18
113112, 93cfv 5589 . . . . . . . . . . . . . . . . 17
114113, 11cfv 5589 . . . . . . . . . . . . . . . 16
115109, 114wceq 1452 . . . . . . . . . . . . . . 15
116 cmin 9880 . . . . . . . . . . . . . . . . 17
11798, 89, 116co 6308 . . . . . . . . . . . . . . . 16
118 cfz 11810 . . . . . . . . . . . . . . . 16
11989, 117, 118co 6308 . . . . . . . . . . . . . . 15
120115, 105, 119wral 2756 . . . . . . . . . . . . . 14
12197, 104, 120w3a 1007 . . . . . . . . . . . . 13
12217, 17cxp 4837 . . . . . . . . . . . . . 14
12389, 98, 118co 6308 . . . . . . . . . . . . . 14
124 cmap 7490 . . . . . . . . . . . . . 14
125122, 123, 124co 6308 . . . . . . . . . . . . 13
126121, 90, 125crab 2760 . . . . . . . . . . . 12
127 cxrs 15476 . . . . . . . . . . . . 13
1286, 83cfv 5589 . . . . . . . . . . . . . 14
12988cv 1451 . . . . . . . . . . . . . 14
130128, 129ccom 4843 . . . . . . . . . . . . 13
131 cgsu 15417 . . . . . . . . . . . . 13 g
132127, 130, 131co 6308 . . . . . . . . . . . 12 g
13388, 126, 132cmpt 4454 . . . . . . . . . . 11 g
134133crn 4840 . . . . . . . . . 10 g
13586, 87, 134ciun 4269 . . . . . . . . 9 g
136 cxr 9692 . . . . . . . . 9
137 clt 9693 . . . . . . . . 9
138135, 136, 137cinf 7973 . . . . . . . 8 inf g
13949, 85, 12, 12, 138cmpt2 6310 . . . . . . 7 inf g
14084, 139cop 3965 . . . . . 6 inf g
14175, 82, 140ctp 3963 . . . . 5 TopSet qTop inf g
14268, 141cun 3388 . . . 4 Scalar Scalar Scalar TopSet qTop inf g
1435, 8, 142csb 3349 . . 3 Scalar Scalar Scalar TopSet qTop inf g
1442, 3, 4, 4, 143cmpt2 6310 . 2 Scalar Scalar Scalar TopSet qTop inf g
1451, 144wceq 1452 1 s Scalar Scalar Scalar TopSet qTop inf g
 Colors of variables: wff setvar class This definition is referenced by:  imasval  15489
 Copyright terms: Public domain W3C validator