Search for blocks/addresses/...
Proofgold Proof
pf
Apply unknownprop_1406677f0460d5e610e1d51da3b7548f6b94ae5487a864770cbbc36f240c53d4 with
equip
(
setminus
(
setprod
u6
u6
)
(
Sing
(
lam
2
(
λ x0 .
If_i
(
x0
=
0
)
u5
u5
)
)
)
)
u35
.
Let x0 of type
ι
→
ι
be given.
Assume H0:
bij
(
setprod
u6
u6
)
u36
x0
.
Apply H0 with
equip
(
setminus
(
setprod
u6
u6
)
(
Sing
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
)
)
u35
.
Assume H1:
and
(
∀ x1 .
x1
∈
setprod
u6
u6
⟶
x0
x1
∈
u36
)
(
∀ x1 .
x1
∈
setprod
u6
u6
⟶
∀ x2 .
x2
∈
setprod
u6
u6
⟶
x0
x1
=
x0
x2
⟶
x1
=
x2
)
.
Apply H1 with
(
∀ x1 .
x1
∈
u36
⟶
∃ x2 .
and
(
x2
∈
setprod
u6
u6
)
(
x0
x2
=
x1
)
)
⟶
equip
(
setminus
(
setprod
u6
u6
)
(
Sing
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
)
)
u35
.
Assume H2:
∀ x1 .
x1
∈
setprod
u6
u6
⟶
x0
x1
∈
u36
.
Assume H3:
∀ x1 .
x1
∈
setprod
u6
u6
⟶
∀ x2 .
x2
∈
setprod
u6
u6
⟶
x0
x1
=
x0
x2
⟶
x1
=
x2
.
Assume H4:
∀ x1 .
x1
∈
u36
⟶
∃ x2 .
and
(
x2
∈
setprod
u6
u6
)
(
x0
x2
=
x1
)
.
Claim L5:
...
...
Claim L6:
...
...
Claim L7:
x0
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
∈
u36
Apply H2 with
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
...
...
)
.
...
Apply equip_tra with
setminus
(
setprod
u6
u6
)
(
Sing
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
)
,
setminus
u36
(
Sing
(
x0
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
)
)
,
u35
leaving 2 subgoals.
Let x1 of type
ο
be given.
Assume H8:
∀ x2 :
ι → ι
.
bij
(
setminus
(
setprod
u6
u6
)
(
Sing
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
u5
u5
)
)
)
)
(
setminus
u36
(
Sing
(
x0
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
u5
u5
)
)
)
)
)
x2
⟶
x1
.
Apply H8 with
x0
.
Apply unknownprop_20ec276501d9ecb91e40cc4525c5a2c0798ab59924056be0d591bc4dcbb72338 with
setprod
u6
u6
,
u36
,
lam
2
(
λ x2 .
If_i
(
x2
=
0
)
u5
u5
)
,
x0
leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H0.
Apply equip_sym with
u35
,
setminus
u36
(
Sing
(
x0
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
)
)
.
Apply unknownprop_6f2f2ee827c101dfeaaaeb47a7a909e08072923ce7f6e05ca4a992c53bc3f486 with
u35
,
x0
(
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
u5
u5
)
)
leaving 2 subgoals.
The subproof is completed by applying unknownprop_a3e012c06fe7317676acef57a26f1aa9ca775c2316f0b3234deabb524335c66f.
The subproof is completed by applying L7.
■