Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for ML
Cartesian exponentiation
finxp2o
Next ⟩
finxp3o
Metamath Proof Explorer
Ascii
Unicode
Theorem
finxp2o
Description:
The value of Cartesian exponentiation at two.
(Contributed by
ML
, 19-Oct-2020)
Ref
Expression
Assertion
finxp2o
⊢
U
↑↑
2
𝑜
=
U
×
U
Proof
Step
Hyp
Ref
Expression
1
df-2o
⊢
2
𝑜
=
suc
⁡
1
𝑜
2
finxpeq2
⊢
2
𝑜
=
suc
⁡
1
𝑜
→
U
↑↑
2
𝑜
=
U
↑↑
suc
⁡
1
𝑜
3
1
2
ax-mp
⊢
U
↑↑
2
𝑜
=
U
↑↑
suc
⁡
1
𝑜
4
1onn
⊢
1
𝑜
∈
ω
5
1n0
⊢
1
𝑜
≠
∅
6
finxpsuc
⊢
1
𝑜
∈
ω
∧
1
𝑜
≠
∅
→
U
↑↑
suc
⁡
1
𝑜
=
U
↑↑
1
𝑜
×
U
7
4
5
6
mp2an
⊢
U
↑↑
suc
⁡
1
𝑜
=
U
↑↑
1
𝑜
×
U
8
finxp1o
⊢
U
↑↑
1
𝑜
=
U
9
8
xpeq1i
⊢
U
↑↑
1
𝑜
×
U
=
U
×
U
10
3
7
9
3eqtri
⊢
U
↑↑
2
𝑜
=
U
×
U