Mathbox for ML |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-finxp | Structured version Visualization version Unicode version |
Description: Define Cartesian
exponentiation on a class.
Note that this definition is limited to finite exponents, since it is defined using nested ordered pairs. If tuples of infinite length are needed, or if they might be needed in the future, use df-ixp 7909 or df-map 7859 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if is a subset of , then df-br 4654 can be used on it, and df-fv 5896 can also be used, and so on. It's also worth keeping in mind that is generally not equal to . This definition is technical. Use finxp1o 33229 and finxpsuc 33235 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.) |
Ref | Expression |
---|---|
df-finxp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cU | . . 3 | |
2 | cN | . . 3 | |
3 | 1, 2 | cfinxp 33220 | . 2 |
4 | com 7065 | . . . . 5 | |
5 | 2, 4 | wcel 1990 | . . . 4 |
6 | c0 3915 | . . . . 5 | |
7 | vn | . . . . . . . 8 | |
8 | vx | . . . . . . . 8 | |
9 | cvv 3200 | . . . . . . . 8 | |
10 | 7 | cv 1482 | . . . . . . . . . . 11 |
11 | c1o 7553 | . . . . . . . . . . 11 | |
12 | 10, 11 | wceq 1483 | . . . . . . . . . 10 |
13 | 8 | cv 1482 | . . . . . . . . . . 11 |
14 | 13, 1 | wcel 1990 | . . . . . . . . . 10 |
15 | 12, 14 | wa 384 | . . . . . . . . 9 |
16 | 9, 1 | cxp 5112 | . . . . . . . . . . 11 |
17 | 13, 16 | wcel 1990 | . . . . . . . . . 10 |
18 | 10 | cuni 4436 | . . . . . . . . . . 11 |
19 | c1st 7166 | . . . . . . . . . . . 12 | |
20 | 13, 19 | cfv 5888 | . . . . . . . . . . 11 |
21 | 18, 20 | cop 4183 | . . . . . . . . . 10 |
22 | 10, 13 | cop 4183 | . . . . . . . . . 10 |
23 | 17, 21, 22 | cif 4086 | . . . . . . . . 9 |
24 | 15, 6, 23 | cif 4086 | . . . . . . . 8 |
25 | 7, 8, 4, 9, 24 | cmpt2 6652 | . . . . . . 7 |
26 | vy | . . . . . . . . 9 | |
27 | 26 | cv 1482 | . . . . . . . 8 |
28 | 2, 27 | cop 4183 | . . . . . . 7 |
29 | 25, 28 | crdg 7505 | . . . . . 6 |
30 | 2, 29 | cfv 5888 | . . . . 5 |
31 | 6, 30 | wceq 1483 | . . . 4 |
32 | 5, 31 | wa 384 | . . 3 |
33 | 32, 26 | cab 2608 | . 2 |
34 | 3, 33 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: dffinxpf 33222 finxpeq1 33223 finxpeq2 33224 csbfinxpg 33225 finxp0 33228 finxp1o 33229 finxpnom 33238 |
Copyright terms: Public domain | W3C validator |