Search for blocks/addresses/...
Proofgold Asset
asset id
8949f950d95391304ad62ef8476eab32210266e2c14fddf77c462e87a9e6fbae
asset hash
bd8d30ef7aaf22be055b3ce79468fc175dd68dc739fe8686af450df62656e2b5
bday / block
1339
tx
dda19..
preasset
doc published by
PrGxv..
Known
b3824..
set_ext
:
∀ x0 x1 .
Subq
x0
x1
⟶
Subq
x1
x0
⟶
x0
=
x1
Known
b0dce..
SubqI
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x0
⟶
In
x2
x1
)
⟶
Subq
x0
x1
Theorem
535f2..
set_ext_2
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x0
⟶
In
x2
x1
)
⟶
(
∀ x2 .
In
x2
x1
⟶
In
x2
x0
)
⟶
x0
=
x1
(proof)
Known
8106d..
notI
:
∀ x0 : ο .
(
x0
⟶
False
)
⟶
not
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Theorem
73fda..
neq_sym_i
:
∀ x0 x1 .
not
(
x0
=
x1
)
⟶
not
(
x1
=
x0
)
(proof)
Theorem
3b206..
tab_neq_i_sym
:
∀ x0 x1 .
not
(
x0
=
x1
)
⟶
(
not
(
x1
=
x0
)
⟶
False
)
⟶
False
(proof)
Known
47706..
xmcases
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
not
x0
⟶
x1
)
⟶
x1
Known
4cb75..
Eps_i_R
:
∀ x0 :
ι → ο
.
∀ x1 .
x0
x1
⟶
x0
(
Eps_i
x0
)
Theorem
9c6aa..
tab_Eps_i
:
∀ x0 :
ι → ο
.
(
(
∀ x1 .
not
(
x0
x1
)
)
⟶
False
)
⟶
(
x0
(
Eps_i
x0
)
⟶
False
)
⟶
False
(proof)
Known
bc395..
If_i_def
:
If_i
=
λ x1 : ο .
λ x2 x3 .
Eps_i
(
λ x4 .
or
(
and
x1
(
x4
=
x2
)
)
(
and
(
not
x1
)
(
x4
=
x3
)
)
)
Known
dcbd9..
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
7c02f..
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
eca40..
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Theorem
66ffc..
:
∀ x0 : ο .
∀ x1 x2 .
or
(
and
x0
(
If_i
x0
x1
x2
=
x1
)
)
(
and
(
not
x0
)
(
If_i
x0
x1
x2
=
x2
)
)
(proof)
Known
37124..
orE
:
∀ x0 x1 : ο .
or
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
andE
andE
:
∀ x0 x1 : ο .
and
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Theorem
22cc3..
:
∀ x0 : ο .
∀ x1 x2 .
∀ x3 : ο .
(
x0
⟶
If_i
x0
x1
x2
=
x1
⟶
x3
)
⟶
(
not
x0
⟶
If_i
x0
x1
x2
=
x2
⟶
x3
)
⟶
x3
(proof)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Theorem
81513..
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
(proof)
Theorem
0d2f9..
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
(proof)
Theorem
e01bb..
If_i_or
:
∀ x0 : ο .
∀ x1 x2 .
or
(
If_i
x0
x1
x2
=
x1
)
(
If_i
x0
x1
x2
=
x2
)
(proof)
Theorem
d99e3..
tab_If_i_lhs
:
∀ x0 : ο .
∀ x1 x2 x3 .
not
(
If_i
x0
x1
x2
=
x3
)
⟶
(
x0
⟶
not
(
x1
=
x3
)
⟶
False
)
⟶
(
not
x0
⟶
not
(
x2
=
x3
)
⟶
False
)
⟶
False
(proof)
Theorem
bafdb..
tab_If_i_rhs
:
∀ x0 : ο .
∀ x1 x2 x3 .
not
(
x3
=
If_i
x0
x1
x2
)
⟶
(
x0
⟶
not
(
x3
=
x1
)
⟶
False
)
⟶
(
not
x0
⟶
not
(
x3
=
x2
)
⟶
False
)
⟶
False
(proof)
Known
74a75..
ReplE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
Repl
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
x2
=
x1
x4
)
⟶
x3
)
⟶
x3
Known
c471b..
UPair_def
:
UPair
=
λ x1 x2 .
Repl
(
Power
(
Power
0
)
)
(
λ x3 .
If_i
(
In
0
x3
)
x1
x2
)
Known
eb789..
andER
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x1
Theorem
469e5..
UPairE
:
∀ x0 x1 x2 .
In
x0
(
UPair
x1
x2
)
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
(proof)
Theorem
7aad1..
UPairE_cases
:
∀ x0 x1 x2 .
In
x0
(
UPair
x1
x2
)
⟶
∀ x3 : ο .
(
x0
=
x1
⟶
x3
)
⟶
(
x0
=
x2
⟶
x3
)
⟶
x3
(proof)
Known
f2c89..
Empty_In_Power
:
∀ x0 .
In
0
(
Power
x0
)
Known
f1bf4..
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
x0
⟶
In
(
x1
x2
)
(
Repl
x0
x1
)
Known
7b5f8..
Self_In_Power
:
∀ x0 .
In
x0
(
Power
x0
)
Theorem
69fe1..
UPairI1
:
∀ x0 x1 .
In
x0
(
UPair
x0
x1
)
(proof)
Known
2901c..
EmptyE
:
∀ x0 .
In
x0
0
⟶
False
Theorem
7477d..
UPairI2
:
∀ x0 x1 .
In
x1
(
UPair
x0
x1
)
(proof)
Theorem
a441e..
:
∀ x0 x1 .
Subq
(
UPair
x0
x1
)
(
UPair
x1
x0
)
(proof)
Theorem
a4584..
UPair_com
:
∀ x0 x1 .
UPair
x0
x1
=
UPair
x1
x0
(proof)
Theorem
aa2ac..
tab_pos_UPair
:
∀ x0 x1 x2 .
In
x2
(
UPair
x0
x1
)
⟶
(
x2
=
x0
⟶
False
)
⟶
(
x2
=
x1
⟶
False
)
⟶
False
(proof)
Known
24526..
nIn_E2
:
∀ x0 x1 .
nIn
x0
x1
⟶
In
x0
x1
⟶
False
Theorem
00e5e..
tab_neg_UPair
:
∀ x0 x1 x2 .
nIn
x2
(
UPair
x0
x1
)
⟶
(
not
(
x2
=
x0
)
⟶
not
(
x2
=
x1
)
⟶
False
)
⟶
False
(proof)
Known
58f30..
Sing_def
:
Sing
=
λ x1 .
UPair
x1
x1
Theorem
1f15b..
SingI
:
∀ x0 .
In
x0
(
Sing
x0
)
(proof)
Theorem
9ae18..
SingE
:
∀ x0 x1 .
In
x1
(
Sing
x0
)
⟶
x1
=
x0
(proof)
Theorem
5d18f..
tab_pos_Sing
:
∀ x0 x1 .
In
x1
(
Sing
x0
)
⟶
(
x1
=
x0
⟶
False
)
⟶
False
(proof)
Theorem
999dc..
tab_neg_Sing
:
∀ x0 x1 .
nIn
x1
(
Sing
x0
)
⟶
(
not
(
x1
=
x0
)
⟶
False
)
⟶
False
(proof)
Known
ba2d5..
binunion_def
:
binunion
=
λ x1 x2 .
Union
(
UPair
x1
x2
)
Known
a4d26..
UnionI
:
∀ x0 x1 x2 .
In
x1
x2
⟶
In
x2
x0
⟶
In
x1
(
Union
x0
)
Theorem
0ce8c..
binunionI1
:
∀ x0 x1 x2 .
In
x2
x0
⟶
In
x2
(
binunion
x0
x1
)
(proof)
Theorem
eb8b4..
binunionI2
:
∀ x0 x1 x2 .
In
x2
x1
⟶
In
x2
(
binunion
x0
x1
)
(proof)
Known
2109a..
UnionE2
:
∀ x0 x1 .
In
x1
(
Union
x0
)
⟶
∀ x2 : ο .
(
∀ x3 .
In
x1
x3
⟶
In
x3
x0
⟶
x2
)
⟶
x2
Theorem
e9b2c..
binunionE
:
∀ x0 x1 x2 .
In
x2
(
binunion
x0
x1
)
⟶
or
(
In
x2
x0
)
(
In
x2
x1
)
(proof)
Theorem
f9974..
binunionE_cases
:
∀ x0 x1 x2 .
In
x2
(
binunion
x0
x1
)
⟶
∀ x3 : ο .
(
In
x2
x0
⟶
x3
)
⟶
(
In
x2
x1
⟶
x3
)
⟶
x3
(proof)
Theorem
1a63b..
tab_pos_binunion
:
∀ x0 x1 x2 .
In
x2
(
binunion
x0
x1
)
⟶
(
In
x2
x0
⟶
False
)
⟶
(
In
x2
x1
⟶
False
)
⟶
False
(proof)
Known
9d2e6..
nIn_I2
:
∀ x0 x1 .
(
In
x0
x1
⟶
False
)
⟶
nIn
x0
x1
Theorem
1954c..
tab_neg_binunion
:
∀ x0 x1 x2 .
nIn
x2
(
binunion
x0
x1
)
⟶
(
nIn
x2
x0
⟶
nIn
x2
x1
⟶
False
)
⟶
False
(proof)
Known
d6778..
Empty_Subq_eq
:
∀ x0 .
Subq
x0
0
⟶
x0
=
0
Known
ae89b..
PowerE
:
∀ x0 x1 .
In
x1
(
Power
x0
)
⟶
Subq
x1
x0
Theorem
1b18d..
Power_0_Sing_0
:
Power
0
=
Sing
0
(proof)
Known
0f096..
ReplE2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
Repl
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
In
x4
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Theorem
62bc0..
Repl_UPair
:
∀ x0 :
ι → ι
.
∀ x1 x2 .
Repl
(
UPair
x1
x2
)
x0
=
UPair
(
x0
x1
)
(
x0
x2
)
(proof)
Theorem
93e44..
Repl_Sing
:
∀ x0 :
ι → ι
.
∀ x1 .
Repl
(
Sing
x1
)
x0
=
Sing
(
x0
x1
)
(proof)
Known
d6d60..
famunion_def
:
famunion
=
λ x1 .
λ x2 :
ι → ι
.
Union
(
Repl
x1
x2
)
Theorem
8f8c2..
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
In
x2
x0
⟶
In
x3
(
x1
x2
)
⟶
In
x3
(
famunion
x0
x1
)
(proof)
Theorem
390bb..
famunionE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
famunion
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
In
x2
(
x1
x4
)
)
⟶
x3
)
⟶
x3
(proof)
Theorem
7b31d..
famunionE2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
famunion
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
In
x4
x0
⟶
In
x2
(
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
40534..
UnionEq_famunionId
:
∀ x0 .
Union
x0
=
famunion
x0
(
λ x2 .
x2
)
(proof)
Theorem
1844d..
ReplEq_famunion_Sing
:
∀ x0 .
∀ x1 :
ι → ι
.
Repl
x0
x1
=
famunion
x0
(
λ x3 .
Sing
(
x1
x3
)
)
(proof)
Theorem
db4b2..
tab_pos_famunion
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
famunion
x0
x1
)
⟶
(
∀ x3 .
In
x3
x0
⟶
In
x2
(
x1
x3
)
⟶
False
)
⟶
False
(proof)
Known
085e3..
contra_In
:
∀ x0 x1 .
(
nIn
x0
x1
⟶
False
)
⟶
In
x0
x1
Theorem
e3f8b..
tab_neg_famunion
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
nIn
x2
(
famunion
x0
x1
)
⟶
(
nIn
x3
x0
⟶
False
)
⟶
(
nIn
x2
(
x1
x3
)
⟶
False
)
⟶
False
(proof)