Search for blocks/addresses/...
Proofgold Asset
asset id
2b01fcb531ced3bf20d78789fae9ec13cb755eec9d9fa564d41d6715adb86838
asset hash
315e677fc8dd13b09585204a3940a78beb2354d467776205924c7c57beb55e5b
bday / block
5952
tx
e2109..
preasset
doc published by
Pr6Pc..
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
Known
Sep_In_Power
Sep_In_Power
:
∀ x0 .
∀ x1 :
ι → ο
.
Sep
x0
x1
∈
prim4
x0
Theorem
KnasterTarski_set
KnasterTarski_set
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
prim4
x0
⟶
x1
x2
∈
prim4
x0
)
⟶
(
∀ x2 .
x2
∈
prim4
x0
⟶
∀ x3 .
x3
∈
prim4
x0
⟶
x2
⊆
x3
⟶
x1
x2
⊆
x1
x3
)
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
prim4
x0
)
(
x1
x3
=
x3
)
⟶
x2
)
⟶
x2
(proof)
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Theorem
image_In_Power
image_In_Power
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
⟶
∀ x3 .
x3
∈
prim4
x0
⟶
prim5
x3
x2
∈
prim4
x1
(proof)
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
image_monotone
image_monotone
:
∀ x0 :
ι → ι
.
∀ x1 x2 .
x1
⊆
x2
⟶
prim5
x1
x0
⊆
prim5
x2
x0
(proof)
Param
setminus
setminus
:
ι
→
ι
→
ι
Known
setminus_Subq
setminus_Subq
:
∀ x0 x1 .
setminus
x0
x1
⊆
x0
Theorem
setminus_In_Power
setminus_In_Power
:
∀ x0 x1 .
setminus
x0
x1
∈
prim4
x0
(proof)
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
setminusE
setminusE
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
and
(
x2
∈
x0
)
(
nIn
x2
x1
)
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Theorem
setminus_antimonotone
setminus_antimonotone
:
∀ x0 x1 x2 .
x1
⊆
x2
⟶
setminus
x0
x2
⊆
setminus
x0
x1
(proof)
Definition
inj
inj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
inv
inv
:
ι
→
(
ι
→
ι
) →
ι
→
ι
Known
bijI
bijI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
⟶
bij
x0
x1
x2
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
inj_linv_coddep
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
∀ x3 .
x3
∈
x0
⟶
inv
x0
x2
(
x2
x3
)
=
x3
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Theorem
SchroederBernstein
SchroederBernstein
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
inj
x0
x1
x2
⟶
inj
x1
x0
x3
⟶
equip
x0
x1
(proof)