Search for blocks/addresses/...
Proofgold Address
address
PUaSf3xGtPXwkdXZz1jipUvBZU2geuRTkZz
total
0
mg
-
conjpub
-
current assets
f0180..
/
a53bf..
bday:
22364
doc published by
PrBPC..
Known
429a0..
equip_mod_I1
:
∀ x0 x1 x2 x3 x4 .
equip
(
setsum
x0
x3
)
x1
⟶
equip
(
setprod
x4
x3
)
x2
⟶
equip_mod
x0
x1
x2
Known
30edc..
equip_tra
:
∀ x0 x1 x2 .
equip
x0
x1
⟶
equip
x1
x2
⟶
equip
x0
x2
Known
637fd..
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Known
c9b7c..
equipE_impred
:
∀ x0 x1 .
equip
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Known
80a11..
bijE_impred
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
∀ x3 : ο .
(
inj
x0
x1
x2
⟶
(
∀ x4 .
In
x4
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
In
x6
x0
)
(
x2
x6
=
x4
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
Known
e6daf..
injE_impred
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
inj
x0
x1
x2
⟶
∀ x3 : ο .
(
(
∀ x4 .
In
x4
x0
⟶
In
(
x2
x4
)
x1
)
⟶
(
∀ x4 .
In
x4
x0
⟶
∀ x5 .
In
x5
x0
⟶
x2
x4
=
x2
x5
⟶
x4
=
x5
)
⟶
x3
)
⟶
x3
Known
f2c5c..
equipI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
equip
x0
x1
Known
e5c63..
bijI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
inj
x0
x1
x2
⟶
(
∀ x3 .
In
x3
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
In
x5
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
⟶
bij
x0
x1
x2
Known
1796e..
injI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
In
x3
x0
⟶
In
(
x2
x3
)
x1
)
⟶
(
∀ x3 .
In
x3
x0
⟶
∀ x4 .
In
x4
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
inj
x0
x1
x2
Known
b4776..
ordsuccE_impred
:
∀ x0 x1 .
In
x1
(
ordsucc
x0
)
⟶
∀ x2 : ο .
(
In
x1
x0
⟶
x2
)
⟶
(
x1
=
x0
⟶
x2
)
⟶
x2
Known
0d2f9..
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
93236..
Inj0_setsum
:
∀ x0 x1 x2 .
In
x2
x0
⟶
In
(
Inj0
x2
)
(
setsum
x0
x1
)
Known
81513..
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
9ea3e..
Inj1_setsum
:
∀ x0 x1 x2 .
In
x2
x1
⟶
In
(
Inj1
x2
)
(
setsum
x0
x1
)
Known
0978b..
In_0_1
:
In
0
1
Known
49afe..
Inj0_inj
:
∀ x0 x1 .
Inj0
x0
=
Inj0
x1
⟶
x0
=
x1
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Known
efcec..
Inj0_Inj1_neq
:
∀ x0 x1 .
not
(
Inj0
x0
=
Inj1
x1
)
Known
26db0..
setsum_def
:
setsum
=
λ x1 x2 .
binunion
(
Repl
x1
Inj0
)
(
Repl
x2
Inj1
)
Known
f9974..
binunionE_cases
:
∀ x0 x1 x2 .
In
x2
(
binunion
x0
x1
)
⟶
∀ x3 : ο .
(
In
x2
x0
⟶
x3
)
⟶
(
In
x2
x1
⟶
x3
)
⟶
x3
Known
0f096..
ReplE2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
Repl
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
In
x4
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
andE
andE
:
∀ x0 x1 : ο .
and
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
7c02f..
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
e9b50..
ordsuccI1b
:
∀ x0 x1 .
In
x1
x0
⟶
In
x1
(
ordsucc
x0
)
Known
cf025..
ordsuccI2
:
∀ x0 .
In
x0
(
ordsucc
x0
)
Known
e51a8..
cases_1
:
∀ x0 .
In
x0
1
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
x0
Known
681fa..
proj0_setprod
:
∀ x0 x1 x2 .
In
x2
(
setprod
x0
x1
)
⟶
In
(
proj0
x2
)
x0
Known
c1504..
tuple_setprod_eta
:
∀ x0 x1 x2 .
In
x2
(
setprod
x0
x1
)
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
ap
x2
0
)
(
ap
x2
1
)
)
=
x2
Known
82f37..
proj0_ap_0
:
∀ x0 .
proj0
x0
=
ap
x0
0
Known
9ae18..
SingE
:
∀ x0 x1 .
In
x1
(
Sing
x0
)
⟶
x1
=
x0
Known
5c344..
eq_1_Sing0
:
1
=
Sing
0
Known
6789e..
ap1_setprod
:
∀ x0 x1 x2 .
In
x2
(
setprod
x0
x1
)
⟶
In
(
ap
x2
1
)
x1
Known
07808..
pair_setprod
:
∀ x0 x1 x2 .
In
x2
x0
⟶
∀ x3 .
In
x3
x1
⟶
In
(
setsum
x2
x3
)
(
setprod
x0
x1
)
Known
d6e1a..
proj0_pair_eq
:
∀ x0 x1 .
proj0
(
setsum
x0
x1
)
=
x0
Known
8106d..
notI
:
∀ x0 : ο .
(
x0
⟶
False
)
⟶
not
x0
Known
2a3a3..
In_irref_b
:
∀ x0 .
In
x0
x0
⟶
False
Theorem
a84bb..
:
∀ x0 x1 x2 x3 .
equip
x0
x3
⟶
equip
x1
(
ordsucc
x3
)
⟶
equip_mod
x0
x1
x2
(proof)
Known
dd0ac..
equip_mod_I2
:
∀ x0 x1 x2 x3 x4 .
equip
(
setsum
x1
x3
)
x0
⟶
equip
(
setprod
x4
x3
)
x2
⟶
equip_mod
x0
x1
x2
Theorem
2931a..
:
∀ x0 x1 x2 x3 .
equip
x0
(
ordsucc
x3
)
⟶
equip
x1
x3
⟶
equip_mod
x0
x1
x2
(proof)
Known
2901c..
EmptyE
:
∀ x0 .
In
x0
0
⟶
False
Known
bc2f0..
ap_setexp
:
∀ x0 x1 x2 .
In
x2
(
setexp
x1
x0
)
⟶
∀ x3 .
In
x3
x0
⟶
In
(
ap
x2
x3
)
x1
Theorem
2fe73..
:
∀ x0 x1 .
In
x1
x0
⟶
equip
(
setexp
0
x0
)
0
(proof)
Known
eead0..
setexp_ext
:
∀ x0 x1 x2 .
In
x2
(
setexp
x1
x0
)
⟶
∀ x3 .
In
x3
(
setexp
x1
x0
)
⟶
(
∀ x4 .
In
x4
x0
⟶
ap
x2
x4
=
ap
x3
x4
)
⟶
x2
=
x3
Known
3152e..
lam_setexp
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
In
x3
x0
⟶
In
(
x2
x3
)
x1
)
⟶
In
(
lam
x0
x2
)
(
setexp
x1
x0
)
Theorem
f186e..
:
∀ x0 .
equip
(
setexp
1
x0
)
1
(proof)
Param
69aae..
exp_nat
:
ι
→
ι
→
ι
Known
d5467..
equip_setexp_ordsucc_setprod
:
∀ x0 x1 .
equip
(
setexp
x1
(
ordsucc
x0
)
)
(
setprod
x1
(
setexp
x1
x0
)
)
Known
f4890..
exp_nat_S
:
∀ x0 x1 .
nat_p
x1
⟶
69aae..
x0
(
ordsucc
x1
)
=
mul_nat
x0
(
69aae..
x0
x1
)
Known
912b9..
equip_setprod_mul_nat_2
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 x3 .
equip
x2
x0
⟶
equip
x3
x1
⟶
equip
(
setprod
x2
x3
)
(
mul_nat
x0
x1
)
Known
2f247..
exp_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
69aae..
x0
x1
)
Known
21472..
equip_setexp_3
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
equip
x1
x0
⟶
equip
(
setexp
x1
3
)
(
69aae..
x0
3
)
Known
21479..
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Known
36841..
nat_2
:
nat_p
2
Theorem
060d0..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
equip
x1
x0
⟶
equip
(
setexp
x1
4
)
(
69aae..
x0
4
)
(proof)
Known
fa8b5..
Sep_In_Power
:
∀ x0 .
∀ x1 :
ι → ο
.
In
(
Sep
x0
x1
)
(
Power
x0
)
Known
3ad28..
cases_2
:
∀ x0 .
In
x0
2
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
x0
Known
dab1f..
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
In
x2
x0
⟶
x1
x2
⟶
In
x2
(
Sep
x0
x1
)
Known
e3ec9..
neq_0_1
:
not
(
0
=
1
)
Known
076ba..
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
In
x2
(
Sep
x0
x1
)
⟶
x1
x2
Known
47706..
xmcases
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
not
x0
⟶
x1
)
⟶
x1
Known
0a117..
In_1_2
:
In
1
2
Known
0863e..
In_0_2
:
In
0
2
Known
535f2..
set_ext_2
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x0
⟶
In
x2
x1
)
⟶
(
∀ x2 .
In
x2
x1
⟶
In
x2
x0
)
⟶
x0
=
x1
Known
b4782..
contra
:
∀ x0 : ο .
(
not
x0
⟶
False
)
⟶
x0
Known
aa3f4..
SepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
In
x2
(
Sep
x0
x1
)
⟶
∀ x3 : ο .
(
In
x2
x0
⟶
x1
x2
⟶
x3
)
⟶
x3
Known
b515a..
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
Known
decfb..
PowerE2
:
∀ x0 x1 .
In
x1
(
Power
x0
)
⟶
∀ x2 .
In
x2
x1
⟶
In
x2
x0
Theorem
7928f..
:
∀ x0 .
equip
(
setexp
2
x0
)
(
Power
x0
)
(proof)
Known
e8081..
tuple_2_setprod
:
∀ x0 x1 x2 .
In
x2
x0
⟶
∀ x3 .
In
x3
x1
⟶
In
(
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
x2
x3
)
)
(
setprod
x0
x1
)
Known
54d83..
setminusE1
:
∀ x0 x1 x2 .
In
x2
(
setminus
x0
x1
)
⟶
In
x2
x0
Known
abe40..
tuple_2_inj_impred
:
∀ x0 x1 x2 x3 .
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x0
x1
)
=
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
x2
x3
)
⟶
∀ x4 : ο .
(
x0
=
x2
⟶
x1
=
x3
⟶
x4
)
⟶
x4
Known
626dc..
setminusI
:
∀ x0 x1 x2 .
In
x2
x0
⟶
nIn
x2
x1
⟶
In
x2
(
setminus
x0
x1
)
Known
9d2e6..
nIn_I2
:
∀ x0 x1 .
(
In
x0
x1
⟶
False
)
⟶
nIn
x0
x1
Known
24526..
nIn_E2
:
∀ x0 x1 .
nIn
x0
x1
⟶
In
x0
x1
⟶
False
Known
28403..
setminusE2
:
∀ x0 x1 x2 .
In
x2
(
setminus
x0
x1
)
⟶
nIn
x2
x1
Known
1f15b..
SingI
:
∀ x0 .
In
x0
(
Sing
x0
)
Known
fe28a..
ap0_setprod
:
∀ x0 x1 x2 .
In
x2
(
setprod
x0
x1
)
⟶
In
(
ap
x2
0
)
x0
Theorem
06adb..
:
∀ x0 x1 x2 .
In
x2
x1
⟶
equip
(
setexp
x0
x1
)
(
setprod
x0
(
setexp
x0
(
setminus
x1
(
Sing
x2
)
)
)
)
(proof)
Known
d0de4..
Empty_eq
:
∀ x0 .
(
∀ x1 .
nIn
x1
x0
)
⟶
x0
=
0
Theorem
82600..
:
∀ x0 .
equip
x0
0
⟶
x0
=
0
(proof)
Known
fed08..
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
94de7..
exp_nat_0
:
∀ x0 .
69aae..
x0
0
=
1
Theorem
4c6ff..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 x3 .
equip
x2
x0
⟶
equip
x3
x1
⟶
equip
(
setexp
x2
x3
)
(
69aae..
x0
x1
)
(proof)
Known
5fc88..
binrep_def
:
binrep
=
λ x1 x2 .
setsum
x1
(
Power
x2
)
Known
56707..
equip_setsum_add_nat_2
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 x3 .
equip
x2
x0
⟶
equip
x3
x1
⟶
equip
(
setsum
x2
x3
)
(
add_nat
x0
x1
)
Known
54d4b..
equip_ref
:
∀ x0 .
equip
x0
x0
Theorem
d6dd4..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 x3 .
equip
x2
x0
⟶
equip
x3
x1
⟶
equip
(
binrep
x2
x3
)
(
add_nat
x0
(
69aae..
2
x1
)
)
(proof)
Known
08405..
nat_0
:
nat_p
0
Theorem
224e2..
:
∀ x0 .
equip
x0
0
⟶
equip
(
Power
x0
)
1
(proof)
Known
9b388..
mul_nat_1R
:
∀ x0 .
mul_nat
x0
1
=
x0
Theorem
f429f..
:
69aae..
2
1
=
2
(proof)
Known
c7c31..
nat_1
:
nat_p
1
Theorem
e6b7d..
:
∀ x0 .
equip
x0
1
⟶
equip
(
Power
x0
)
2
(proof)
Known
c13d1..
add_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
add_nat
x0
(
ordsucc
x1
)
=
ordsucc
(
add_nat
x0
x1
)
Known
02169..
add_nat_0R
:
∀ x0 .
add_nat
x0
0
=
x0
Theorem
63495..
:
∀ x0 .
add_nat
x0
1
=
ordsucc
x0
(proof)
Theorem
5af12..
:
∀ x0 .
add_nat
x0
2
=
ordsucc
(
ordsucc
x0
)
(proof)
Theorem
0ac77..
:
∀ x0 x1 .
nat_p
x1
⟶
add_nat
x0
(
ordsucc
(
ordsucc
x1
)
)
=
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
(proof)
Theorem
07519..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
x0
)
)
(proof)
Theorem
9814f..
:
nat_p
3
(proof)
Theorem
c83a0..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x0
)
)
)
)
(proof)
Theorem
2b6ba..
:
nat_p
4
(proof)
Theorem
b2788..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x0
)
)
)
)
)
)
)
)
(proof)
Theorem
a2e43..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
74cfe..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
53f67..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
6d362..
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(