Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for ML
Cartesian exponentiation
finxpreclem1
Next ⟩
finxpreclem2
Metamath Proof Explorer
Ascii
Unicode
Theorem
finxpreclem1
Description:
Lemma for
^^
recursion theorems.
(Contributed by
ML
, 17-Oct-2020)
Ref
Expression
Assertion
finxpreclem1
⊢
X
∈
U
→
∅
=
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
⁡
1
𝑜
X
Proof
Step
Hyp
Ref
Expression
1
df-ov
⊢
1
𝑜
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
X
=
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
⁡
1
𝑜
X
2
eqidd
⊢
X
∈
U
→
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
=
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
3
eleq1a
⊢
X
∈
U
→
x
=
X
→
x
∈
U
4
3
anim2d
⊢
X
∈
U
→
n
=
1
𝑜
∧
x
=
X
→
n
=
1
𝑜
∧
x
∈
U
5
iftrue
⊢
n
=
1
𝑜
∧
x
∈
U
→
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
=
∅
6
4
5
syl6
⊢
X
∈
U
→
n
=
1
𝑜
∧
x
=
X
→
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
=
∅
7
6
imp
⊢
X
∈
U
∧
n
=
1
𝑜
∧
x
=
X
→
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
=
∅
8
1onn
⊢
1
𝑜
∈
ω
9
8
a1i
⊢
X
∈
U
→
1
𝑜
∈
ω
10
elex
⊢
X
∈
U
→
X
∈
V
11
0ex
⊢
∅
∈
V
12
11
a1i
⊢
X
∈
U
→
∅
∈
V
13
2
7
9
10
12
ovmpod
⊢
X
∈
U
→
1
𝑜
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
X
=
∅
14
1
13
syl5reqr
⊢
X
∈
U
→
∅
=
n
∈
ω
,
x
∈
V
⟼
if
n
=
1
𝑜
∧
x
∈
U
∅
if
x
∈
V
×
U
⋃
n
1
st
⁡
x
n
x
⁡
1
𝑜
X