Search for blocks/addresses/...
Proofgold Asset
asset id
cd427e3e2051ff0c43e44cb749918761c2ccb34829f4f2f548973befec3e6c92
asset hash
8f355f0f83f346d521fd72e829df4900c6079d741adb7f42b7ab89a51d95e5a0
bday / block
4892
tx
d4a74..
preasset
doc published by
Pr6Pc..
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Theorem
exandE_i
exandE_i
:
∀ x0 x1 :
ι → ο
.
(
∀ x2 : ο .
(
∀ x3 .
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 .
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
(proof)
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
If_Vo4
If_Vo4
:=
λ x0 : ο .
λ x1 x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
λ x3 :
(
(
ι → ο
)
→ ο
)
→ ο
.
and
(
x0
⟶
x1
x3
)
(
not
x0
⟶
x2
x3
)
Known
prop_ext_2
prop_ext_2
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
x0
=
x1
Known
andEL
andEL
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x0
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Theorem
If_Vo4_1
If_Vo4_1
:
∀ x0 : ο .
∀ x1 x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
x0
⟶
If_Vo4
x0
x1
x2
=
x1
(proof)
Known
andER
andER
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x1
Theorem
If_Vo4_0
If_Vo4_0
:
∀ x0 : ο .
∀ x1 x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
not
x0
⟶
If_Vo4
x0
x1
x2
=
x2
(proof)
Definition
Descr_Vo4
Descr_Vo4
:=
λ x0 :
(
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→ ο
.
λ x1 :
(
(
ι → ο
)
→ ο
)
→ ο
.
∀ x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
x0
x2
⟶
x2
x1
Theorem
Descr_Vo4_prop
Descr_Vo4_prop
:
∀ x0 :
(
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x1 : ο .
(
∀ x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
x0
x2
⟶
x1
)
⟶
x1
)
⟶
(
∀ x1 x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
x0
x1
⟶
x0
x2
⟶
x1
=
x2
)
⟶
x0
(
Descr_Vo4
x0
)
(proof)
Definition
461b4..
:=
λ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
λ x1 .
λ x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
∀ x3 :
ι →
(
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x4 .
∀ x5 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_Vo4
In_rec_Vo4
:=
λ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
λ x1 .
Descr_Vo4
(
461b4..
x0
x1
)
Theorem
23e18..
:
∀ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
∀ x1 .
∀ x2 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x3 .
x3
∈
x1
⟶
461b4..
x0
x3
(
x2
x3
)
)
⟶
461b4..
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
45e15..
:
∀ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
∀ x1 .
∀ x2 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
461b4..
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
and
(
∀ x5 .
x5
∈
x1
⟶
461b4..
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Known
In_ind
In_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
x0
x1
Theorem
87941..
:
∀ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
∀ x2 x3 :
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
461b4..
x0
x1
x2
⟶
461b4..
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
6dcc7..
:
∀ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
461b4..
x0
x1
(
In_rec_Vo4
x0
x1
)
(proof)
Theorem
05f75..
:
∀ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
461b4..
x0
x1
(
x0
x1
(
In_rec_Vo4
x0
)
)
(proof)
Theorem
In_rec_Vo4_eq
In_rec_Vo4_eq
:
∀ x0 :
ι →
(
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
)
→
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
(
(
ι → ο
)
→ ο
)
→ ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_Vo4
x0
x1
=
x0
x1
(
In_rec_Vo4
x0
)
(proof)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
not_and_or_demorgan
not_and_or_demorgan
:
∀ x0 x1 : ο .
not
(
and
x0
x1
)
⟶
or
(
not
x0
)
(
not
x1
)
Theorem
eq_imp_or
eq_imp_or
:
(
λ x1 x2 : ο .
x1
⟶
x2
)
=
λ x1 : ο .
or
(
not
x1
)
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
Subq_contra
Subq_contra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
nIn
x2
x1
⟶
nIn
x2
x0
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
Subq_Empty
Subq_Empty
:
∀ x0 .
0
⊆
x0
Known
Empty_Subq_eq
Empty_Subq_eq
:
∀ x0 .
x0
⊆
0
⟶
x0
=
0
Known
Empty_eq
Empty_eq
:
∀ x0 .
(
∀ x1 .
nIn
x1
x0
)
⟶
x0
=
0
Known
UnionE
UnionE
:
∀ x0 x1 .
x1
∈
prim3
x0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x1
∈
x3
)
(
x3
∈
x0
)
⟶
x2
)
⟶
x2
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
Union_Empty
Union_Empty
:
prim3
0
=
0
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Known
Union_Power_Subq
Union_Power_Subq
:
∀ x0 .
prim3
(
prim4
x0
)
⊆
x0
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
Repl_Empty
Repl_Empty
:
∀ x0 :
ι → ι
.
prim5
0
x0
=
0
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Known
ReplEq_ext_sub
ReplEq_ext_sub
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
⊆
prim5
x0
x2
Known
ReplEq_ext
ReplEq_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
=
prim5
x0
x2
Param
UPair
UPair
:
ι
→
ι
→
ι
Known
UPairE
UPairE
:
∀ x0 x1 x2 .
x0
∈
UPair
x1
x2
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
Known
UPairI2
UPairI2
:
∀ x0 x1 .
x1
∈
UPair
x0
x1
Known
UPairI1
UPairI1
:
∀ x0 x1 .
x0
∈
UPair
x0
x1
Known
93b47..
:
∀ x0 x1 .
UPair
x0
x1
⊆
UPair
x1
x0
Known
UPair_com
UPair_com
:
∀ x0 x1 .
UPair
x0
x1
=
UPair
x1
x0
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Definition
SetAdjoin
SetAdjoin
:=
λ x0 x1 .
binunion
x0
(
Sing
x1
)
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
Empty_In_Power
Empty_In_Power
:
∀ x0 .
0
∈
prim4
x0
Known
Power_0_Sing_0
Power_0_Sing_0
:
prim4
0
=
Sing
0
Known
Repl_UPair
Repl_UPair
:
∀ x0 :
ι → ι
.
∀ x1 x2 .
prim5
(
UPair
x1
x2
)
x0
=
UPair
(
x0
x1
)
(
x0
x2
)
Known
Repl_Sing
Repl_Sing
:
∀ x0 :
ι → ι
.
∀ x1 .
prim5
(
Sing
x1
)
x0
=
Sing
(
x0
x1
)
Known
ReplE
ReplE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
x1
x4
)
⟶
x3
)
⟶
x3
Known
ReplEq_ext_sub
ReplEq_ext_sub
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
⊆
prim5
x0
x2
Known
ReplEq_ext
ReplEq_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
=
prim5
x0
x2
Definition
famunion
famunion
:=
λ x0 .
λ x1 :
ι → ι
.
prim3
(
prim5
x0
x1
)
Known
UnionI
UnionI
:
∀ x0 x1 x2 .
x1
∈
x2
⟶
x2
∈
x0
⟶
x1
∈
prim3
x0
Known
famunionI
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
x0
⟶
x3
∈
x1
x2
⟶
x3
∈
famunion
x0
x1
Known
UnionE_impred
UnionE_impred
:
∀ x0 x1 .
x1
∈
prim3
x0
⟶
∀ x2 : ο .
(
∀ x3 .
x1
∈
x3
⟶
x3
∈
x0
⟶
x2
)
⟶
x2
Known
famunionE
famunionE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
∈
x1
x4
)
⟶
x3
)
⟶
x3
Known
famunionE_impred
famunionE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
∈
x1
x4
⟶
x3
)
⟶
x3
Known
UnionEq_famunionId
UnionEq_famunionId
:
∀ x0 .
prim3
x0
=
famunion
x0
(
λ x2 .
x2
)
Known
ReplEq_famunion_Sing
ReplEq_famunion_Sing
:
∀ x0 .
∀ x1 :
ι → ι
.
prim5
x0
x1
=
famunion
x0
(
λ x3 .
Sing
(
x1
x3
)
)
Theorem
Empty_or_ex
Empty_or_ex
:
∀ x0 .
or
(
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
x1
)
⟶
x1
)
(proof)