Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for ML
Cartesian exponentiation
finxpsuc
Next ⟩
finxp2o
Metamath Proof Explorer
Ascii
Unicode
Theorem
finxpsuc
Description:
The value of Cartesian exponentiation at a successor.
(Contributed by
ML
, 24-Oct-2020)
Ref
Expression
Assertion
finxpsuc
⊢
N
∈
ω
∧
N
≠
∅
→
U
↑↑
suc
⁡
N
=
U
↑↑
N
×
U
Proof
Step
Hyp
Ref
Expression
1
nnord
⊢
N
∈
ω
→
Ord
⁡
N
2
ordge1n0
⊢
Ord
⁡
N
→
1
𝑜
⊆
N
↔
N
≠
∅
3
1
2
syl
⊢
N
∈
ω
→
1
𝑜
⊆
N
↔
N
≠
∅
4
3
biimprd
⊢
N
∈
ω
→
N
≠
∅
→
1
𝑜
⊆
N
5
4
imdistani
⊢
N
∈
ω
∧
N
≠
∅
→
N
∈
ω
∧
1
𝑜
⊆
N
6
eqid
⊢
y
∈
ω
,
x
∈
V
⟼
if
y
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
y
1
st
⁡
x
y
x
=
y
∈
ω
,
x
∈
V
⟼
if
y
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
y
1
st
⁡
x
y
x
7
6
finxpsuclem
⊢
N
∈
ω
∧
1
𝑜
⊆
N
→
U
↑↑
suc
⁡
N
=
U
↑↑
N
×
U
8
5
7
syl
⊢
N
∈
ω
∧
N
≠
∅
→
U
↑↑
suc
⁡
N
=
U
↑↑
N
×
U