Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrEvg..
/
6b862..
PUarZ..
/
3d009..
vout
PrEvg..
/
2111f..
8.98 bars
TMUYd..
/
2799c..
ownership of
4862c..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYiJ..
/
f2812..
ownership of
65bac..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLfg..
/
9f1f8..
ownership of
b515a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQuy..
/
a1dc4..
ownership of
c5e21..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQas..
/
9ca1b..
ownership of
d1a05..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TManw..
/
80a5f..
ownership of
e5b51..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMafb..
/
d767e..
ownership of
0bd41..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSzA..
/
74d7a..
ownership of
76235..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZPy..
/
6801a..
ownership of
970d5..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSnz..
/
2c238..
ownership of
57903..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJqr..
/
a3b48..
ownership of
efa2b..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMEW..
/
322c6..
ownership of
337b2..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLKG..
/
7ea04..
ownership of
e3e5f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMEio..
/
02660..
ownership of
f2581..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMic..
/
50a81..
ownership of
f9ff3..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZca..
/
15344..
ownership of
1633a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXon..
/
e8f45..
ownership of
c6ec6..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMF75..
/
e59ce..
ownership of
6708a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPWT..
/
43a0a..
ownership of
98421..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWT4..
/
79fc1..
ownership of
94fdc..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMThT..
/
90b9f..
ownership of
3ea93..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVww..
/
145e1..
ownership of
2e962..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMEyS..
/
57c28..
ownership of
b327e..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTFm..
/
13979..
ownership of
bd618..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVwm..
/
6302e..
ownership of
40531..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcaN..
/
45568..
ownership of
ab3a5..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMEwg..
/
ba5c8..
ownership of
1cfb6..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWVR..
/
f3604..
ownership of
0ca88..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQ3r..
/
a5d5a..
ownership of
681fa..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMY5c..
/
ed517..
ownership of
7f5f9..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSnW..
/
7fe97..
ownership of
07808..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZiU..
/
72132..
ownership of
3ca74..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPcd..
/
0ecb9..
ownership of
71581..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMReW..
/
1a29e..
ownership of
84894..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMZz..
/
cf6b0..
ownership of
251f7..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJsV..
/
233c2..
ownership of
31b47..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXtb..
/
688e5..
ownership of
01b21..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMT18..
/
fa209..
ownership of
cdf99..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMad9..
/
d41b0..
ownership of
1587f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNp7..
/
ce8af..
ownership of
c6406..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJ1Z..
/
52d45..
ownership of
be650..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMEhK..
/
6b643..
ownership of
1675a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTYN..
/
1ddd0..
ownership of
1d863..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVKH..
/
d704d..
ownership of
57691..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSfY..
/
b1887..
ownership of
6bfcf..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGTN..
/
24fb4..
ownership of
90e3c..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMsP..
/
91040..
ownership of
3057f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMG31..
/
9955e..
ownership of
5602d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdoc..
/
2a150..
ownership of
413ee..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTZC..
/
10288..
ownership of
1006f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZwx..
/
dac25..
ownership of
56f17..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQsh..
/
5b9bc..
ownership of
632d5..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLdJ..
/
759d4..
ownership of
8da7f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVJq..
/
463b3..
ownership of
a059c..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMa3o..
/
28e33..
ownership of
a1bad..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQLB..
/
a2e0d..
ownership of
fafba..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMKS7..
/
f9a37..
ownership of
b8fac..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGoU..
/
271ae..
ownership of
d4bb6..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMNj..
/
da10c..
ownership of
d6e1a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLPR..
/
9d776..
ownership of
e2d9d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMKFg..
/
e424e..
ownership of
13e9e..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTff..
/
817fe..
ownership of
ddee3..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPUg..
/
a9a84..
ownership of
16411..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMH4t..
/
76902..
ownership of
83b14..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYsZ..
/
cfb46..
ownership of
88f5c..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSSF..
/
fdb61..
ownership of
5992b..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMRze..
/
608ce..
ownership of
afc0a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNpV..
/
c7cf3..
ownership of
ceb85..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUkr..
/
3516b..
ownership of
2a16a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLMA..
/
bbe22..
ownership of
2edc8..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMEp1..
/
987c7..
ownership of
861bf..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcLY..
/
fa89c..
ownership of
be49f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMKSH..
/
fc2f6..
ownership of
d321a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMaQG..
/
7907b..
ownership of
ba4bb..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFGv..
/
80d57..
ownership of
2a3f2..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMPh..
/
1bd86..
ownership of
976b9..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMN2Q..
/
f27a2..
ownership of
2ce7d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFkz..
/
e8ef2..
ownership of
c5299..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMbYP..
/
69c85..
ownership of
77980..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMKQ..
/
a23c7..
ownership of
ba4ce..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXgK..
/
e1fa1..
ownership of
65c61..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMF3r..
/
b1717..
ownership of
a381a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHvj..
/
8f0f9..
ownership of
715b1..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMR4t..
/
32dc6..
ownership of
e88b1..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNqj..
/
9b4e0..
ownership of
dfb4d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPGt..
/
b470d..
ownership of
74210..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQ5j..
/
9d1f0..
ownership of
0e046..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTCU..
/
4bca1..
ownership of
14a19..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFzi..
/
039f9..
ownership of
9eb99..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdRu..
/
51613..
ownership of
94862..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMKBS..
/
e0ec9..
ownership of
c6ede..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNWX..
/
8d186..
ownership of
32abc..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMbjT..
/
f6566..
ownership of
52346..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTtk..
/
aa49a..
ownership of
92e9d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGE1..
/
717e0..
ownership of
412eb..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMaZR..
/
527b1..
ownership of
8438e..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMbMc..
/
d7542..
ownership of
decfb..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLdf..
/
484ae..
ownership of
80adb..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMG1H..
/
b8b3c..
ownership of
bcb61..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcR6..
/
30b40..
ownership of
db770..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
PUaiy..
/
2e211..
doc published by
PrGxv..
Known
2d44a..
PowerI
:
∀ x0 x1 .
Subq
x1
x0
⟶
In
x1
(
Power
x0
)
Known
b0dce..
SubqI
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x0
⟶
In
x2
x1
)
⟶
Subq
x0
x1
Theorem
bcb61..
PowerI2
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x1
⟶
In
x2
x0
)
⟶
In
x1
(
Power
x0
)
(proof)
Known
367e6..
SubqE
:
∀ x0 x1 .
Subq
x0
x1
⟶
∀ x2 .
In
x2
x0
⟶
In
x2
x1
Known
ae89b..
PowerE
:
∀ x0 x1 .
In
x1
(
Power
x0
)
⟶
Subq
x1
x0
Theorem
decfb..
PowerE2
:
∀ x0 x1 .
In
x1
(
Power
x0
)
⟶
∀ x2 .
In
x2
x1
⟶
In
x2
x0
(proof)
Known
535f2..
set_ext_2
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x0
⟶
In
x2
x1
)
⟶
(
∀ x2 .
In
x2
x1
⟶
In
x2
x0
)
⟶
x0
=
x1
Known
351c1..
setsum_Inj_inv_impred
:
∀ x0 x1 x2 .
In
x2
(
setsum
x0
x1
)
⟶
∀ x3 :
ι → ο
.
(
∀ x4 .
In
x4
x0
⟶
x3
(
Inj0
x4
)
)
⟶
(
∀ x4 .
In
x4
x1
⟶
x3
(
Inj1
x4
)
)
⟶
x3
x2
Known
fc3ab..
Inj0_0
:
Inj0
0
=
0
Known
8d83e..
Inj1I1
:
∀ x0 .
In
0
(
Inj1
x0
)
Known
9ae18..
SingE
:
∀ x0 x1 .
In
x1
(
Sing
x0
)
⟶
x1
=
x0
Known
830d8..
Subq_1_Sing0
:
Subq
1
(
Sing
0
)
Known
22441..
Inj1I2
:
∀ x0 x1 .
In
x1
x0
⟶
In
(
Inj1
x1
)
(
Inj1
x0
)
Known
474ab..
Inj1E_impred
:
∀ x0 x1 .
In
x1
(
Inj1
x0
)
⟶
∀ x2 :
ι → ο
.
x2
0
⟶
(
∀ x3 .
In
x3
x0
⟶
x2
(
Inj1
x3
)
)
⟶
x2
x1
Known
93236..
Inj0_setsum
:
∀ x0 x1 x2 .
In
x2
x0
⟶
In
(
Inj0
x2
)
(
setsum
x0
x1
)
Known
0978b..
In_0_1
:
In
0
1
Known
9ea3e..
Inj1_setsum
:
∀ x0 x1 x2 .
In
x2
x1
⟶
In
(
Inj1
x2
)
(
setsum
x0
x1
)
Theorem
412eb..
Inj1_setsum_1L
:
∀ x0 .
setsum
1
x0
=
Inj1
x0
(proof)
Known
92870..
nat_complete_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
In
x2
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
7bd16..
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
In
0
(
ordsucc
x0
)
Known
840d1..
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
In
x1
x0
⟶
In
(
ordsucc
x1
)
(
ordsucc
x0
)
Known
b4776..
ordsuccE_impred
:
∀ x0 x1 .
In
x1
(
ordsucc
x0
)
⟶
∀ x2 : ο .
(
In
x1
x0
⟶
x2
)
⟶
(
x1
=
x0
⟶
x2
)
⟶
x2
Known
37124..
orE
:
∀ x0 x1 : ο .
or
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
c7246..
nat_inv
:
∀ x0 .
nat_p
x0
⟶
or
(
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
x0
=
ordsucc
x2
)
⟶
x1
)
⟶
x1
)
Known
b0a90..
nat_p_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
In
x1
x0
⟶
nat_p
x1
Known
61640..
exandE_i
:
∀ x0 x1 :
ι → ο
.
(
∀ x2 : ο .
(
∀ x3 .
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 .
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
Known
80da5..
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
In
x1
x0
⟶
Subq
x1
x0
Known
cf025..
ordsuccI2
:
∀ x0 .
In
x0
(
ordsucc
x0
)
Theorem
0e046..
nat_pair1_ordsucc
:
∀ x0 .
nat_p
x0
⟶
setsum
1
x0
=
ordsucc
x0
(proof)
Known
b9c5c..
Inj0_setsum_0L
:
∀ x0 .
setsum
0
x0
=
Inj0
x0
Theorem
52346..
pair_0_0
:
setsum
0
0
=
0
(proof)
Known
08405..
nat_0
:
nat_p
0
Theorem
c6ede..
pair_1_0_1
:
setsum
1
0
=
1
(proof)
Known
c7c31..
nat_1
:
nat_p
1
Theorem
9eb99..
pair_1_1_2
:
setsum
1
1
=
2
(proof)
Theorem
52346..
pair_0_0
:
setsum
0
0
=
0
(proof)
Theorem
c6ede..
pair_1_0_1
:
setsum
1
0
=
1
(proof)
Theorem
9eb99..
pair_1_1_2
:
setsum
1
1
=
2
(proof)
Theorem
0e046..
nat_pair1_ordsucc
:
∀ x0 .
nat_p
x0
⟶
setsum
1
x0
=
ordsucc
x0
(proof)
Known
15e97..
eq_sym_i
:
∀ x0 x1 .
x0
=
x1
⟶
x1
=
x0
Theorem
dfb4d..
Inj0_pair_0_eq
:
Inj0
=
setsum
0
(proof)
Theorem
715b1..
Inj1_pair_1_eq
:
Inj1
=
setsum
1
(proof)
Theorem
65c61..
pairI0
:
∀ x0 x1 x2 .
In
x2
x0
⟶
In
(
setsum
0
x2
)
(
setsum
x0
x1
)
(proof)
Theorem
77980..
pairI1
:
∀ x0 x1 x2 .
In
x2
x1
⟶
In
(
setsum
1
x2
)
(
setsum
x0
x1
)
(proof)
Known
76cef..
setsum_Inj_inv
:
∀ x0 x1 x2 .
In
x2
(
setsum
x0
x1
)
⟶
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
x2
=
Inj0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x1
)
(
x2
=
Inj1
x4
)
⟶
x3
)
⟶
x3
)
Theorem
2ce7d..
pairE
:
∀ x0 x1 x2 .
In
x2
(
setsum
x0
x1
)
⟶
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
x2
=
setsum
0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x1
)
(
x2
=
setsum
1
x4
)
⟶
x3
)
⟶
x3
)
(proof)
Known
andE
andE
:
∀ x0 x1 : ο .
and
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Theorem
2a3f2..
pairE_impred
:
∀ x0 x1 x2 .
In
x2
(
setsum
x0
x1
)
⟶
∀ x3 :
ι → ο
.
(
∀ x4 .
In
x4
x0
⟶
x3
(
setsum
0
x4
)
)
⟶
(
∀ x4 .
In
x4
x1
⟶
x3
(
setsum
1
x4
)
)
⟶
x3
x2
(proof)
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
)
Theorem
d321a..
pairE0
:
∀ x0 x1 x2 .
In
(
setsum
0
x2
)
(
setsum
x0
x1
)
⟶
In
x2
x0
(proof)
Known
0139a..
Inj1_inj
:
∀ x0 x1 .
Inj1
x0
=
Inj1
x1
⟶
x0
=
x1
Theorem
861bf..
pairE1
:
∀ x0 x1 x2 .
In
(
setsum
1
x2
)
(
setsum
x0
x1
)
⟶
In
x2
x1
(proof)
Known
32c82..
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Theorem
2a16a..
pairEq
:
∀ x0 x1 x2 .
iff
(
In
x2
(
setsum
x0
x1
)
)
(
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
x2
=
setsum
0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x1
)
(
x2
=
setsum
1
x4
)
⟶
x3
)
⟶
x3
)
)
(proof)
Theorem
374e6..
pairSubq
:
∀ x0 x1 x2 x3 .
Subq
x0
x2
⟶
Subq
x1
x3
⟶
Subq
(
setsum
x0
x1
)
(
setsum
x2
x3
)
(proof)
Known
92282..
proj0_def
:
proj0
=
λ x1 .
ReplSep
x1
(
λ x2 .
∀ x3 : ο .
(
∀ x4 .
Inj0
x4
=
x2
⟶
x3
)
⟶
x3
)
Unj
Known
c3d4f..
Unj_Inj0_eq
:
∀ x0 .
Unj
(
Inj0
x0
)
=
x0
Known
9fdc4..
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
In
x3
x0
⟶
x1
x3
⟶
In
(
x2
x3
)
(
ReplSep
x0
x1
x2
)
Theorem
afc0a..
proj0I
:
∀ x0 x1 .
In
(
setsum
0
x1
)
x0
⟶
In
x1
(
proj0
x0
)
(proof)
Known
65d0d..
ReplSepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
In
x3
(
ReplSep
x0
x1
x2
)
⟶
∀ x4 : ο .
(
∀ x5 .
In
x5
x0
⟶
x1
x5
⟶
x3
=
x2
x5
⟶
x4
)
⟶
x4
Theorem
88f5c..
proj0E
:
∀ x0 x1 .
In
x1
(
proj0
x0
)
⟶
In
(
setsum
0
x1
)
x0
(proof)
Known
c65ed..
proj1_def
:
proj1
=
λ x1 .
ReplSep
x1
(
λ x2 .
∀ x3 : ο .
(
∀ x4 .
Inj1
x4
=
x2
⟶
x3
)
⟶
x3
)
Unj
Known
c76aa..
Unj_Inj1_eq
:
∀ x0 .
Unj
(
Inj1
x0
)
=
x0
Theorem
16411..
proj1I
:
∀ x0 x1 .
In
(
setsum
1
x1
)
x0
⟶
In
x1
(
proj1
x0
)
(proof)
Theorem
13e9e..
proj1E
:
∀ x0 x1 .
In
x1
(
proj1
x0
)
⟶
In
(
setsum
1
x1
)
x0
(proof)
Theorem
d6e1a..
proj0_pair_eq
:
∀ x0 x1 .
proj0
(
setsum
x0
x1
)
=
x0
(proof)
Theorem
b8fac..
proj1_pair_eq
:
∀ x0 x1 .
proj1
(
setsum
x0
x1
)
=
x1
(proof)
Known
7c02f..
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
a1bad..
pair_inj
:
∀ x0 x1 x2 x3 .
setsum
x0
x1
=
setsum
x2
x3
⟶
and
(
x0
=
x2
)
(
x1
=
x3
)
(proof)
Theorem
8da7f..
pair_eta_Subq_proj
:
∀ x0 .
Subq
(
setsum
(
proj0
x0
)
(
proj1
x0
)
)
x0
(proof)
Known
04d4d..
lam_def
:
lam
=
λ x1 .
λ x2 :
ι → ι
.
famunion
x1
(
λ x3 .
Repl
(
x2
x3
)
(
setsum
x3
)
)
Known
8f8c2..
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
In
x2
x0
⟶
In
x3
(
x1
x2
)
⟶
In
x3
(
famunion
x0
x1
)
Known
f1bf4..
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
x0
⟶
In
(
x1
x2
)
(
Repl
x0
x1
)
Theorem
f9ff3..
lamI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
x0
⟶
∀ x3 .
In
x3
(
x1
x2
)
⟶
In
(
setsum
x2
x3
)
(
lam
x0
x1
)
(proof)
Known
7b31d..
famunionE2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
famunion
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
In
x4
x0
⟶
In
x2
(
x1
x4
)
⟶
x3
)
⟶
x3
Known
0f096..
ReplE2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
Repl
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
In
x4
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
f6404..
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Theorem
56f17..
Sigma_eta_proj0_proj1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
lam
x0
x1
)
⟶
and
(
and
(
setsum
(
proj0
x2
)
(
proj1
x2
)
=
x2
)
(
In
(
proj0
x2
)
x0
)
)
(
In
(
proj1
x2
)
(
x1
(
proj0
x2
)
)
)
(proof)
Known
cd094..
and3E
:
∀ x0 x1 x2 : ο .
and
(
and
x0
x1
)
x2
⟶
∀ x3 : ο .
(
x0
⟶
x1
⟶
x2
⟶
x3
)
⟶
x3
Theorem
413ee..
proj_Sigma_eta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
lam
x0
x1
)
⟶
setsum
(
proj0
x2
)
(
proj1
x2
)
=
x2
(proof)
Theorem
3057f..
proj0_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
lam
x0
x1
)
⟶
In
(
proj0
x2
)
x0
(proof)
Theorem
6bfcf..
proj1_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
lam
x0
x1
)
⟶
In
(
proj1
x2
)
(
x1
(
proj0
x2
)
)
(proof)
Theorem
1d863..
pair_Sigma_E0
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
In
(
setsum
x2
x3
)
(
lam
x0
x1
)
⟶
In
x2
x0
(proof)
Theorem
be650..
pair_Sigma_E1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
In
(
setsum
x2
x3
)
(
lam
x0
x1
)
⟶
In
x3
(
x1
x2
)
(proof)
Theorem
e3e5f..
lamE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
lam
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
In
x6
(
x1
x4
)
)
(
x2
=
setsum
x4
x6
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
(proof)
Theorem
efa2b..
lamEq
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
iff
(
In
x2
(
lam
x0
x1
)
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
In
x6
(
x1
x4
)
)
(
x2
=
setsum
x4
x6
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
)
(proof)
Theorem
1587f..
Sigma_mon
:
∀ x0 x1 .
Subq
x0
x1
⟶
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
In
x4
x0
⟶
Subq
(
x2
x4
)
(
x3
x4
)
)
⟶
Subq
(
lam
x0
x2
)
(
lam
x1
x3
)
(proof)
Known
6696a..
Subq_ref
:
∀ x0 .
Subq
x0
x0
Theorem
01b21..
Sigma_mon0
:
∀ x0 x1 .
Subq
x0
x1
⟶
∀ x2 :
ι → ι
.
Subq
(
lam
x0
x2
)
(
lam
x1
x2
)
(proof)
Theorem
251f7..
Sigma_mon1
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
In
x3
x0
⟶
Subq
(
x1
x3
)
(
x2
x3
)
)
⟶
Subq
(
lam
x0
x1
)
(
lam
x0
x2
)
(proof)
Theorem
71581..
Sigma_Power_1
:
∀ x0 .
In
x0
(
Power
1
)
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
In
x2
x0
⟶
In
(
x1
x2
)
(
Power
1
)
)
⟶
In
(
lam
x0
x1
)
(
Power
1
)
(proof)
Known
ad99c..
setprod_def
:
setprod
=
λ x1 x2 .
lam
x1
(
λ x3 .
x2
)
Theorem
07808..
pair_setprod
:
∀ x0 x1 x2 .
In
x2
x0
⟶
∀ x3 .
In
x3
x1
⟶
In
(
setsum
x2
x3
)
(
setprod
x0
x1
)
(proof)
Theorem
681fa..
proj0_setprod
:
∀ x0 x1 x2 .
In
x2
(
setprod
x0
x1
)
⟶
In
(
proj0
x2
)
x0
(proof)
Theorem
1cfb6..
proj1_setprod
:
∀ x0 x1 x2 .
In
x2
(
setprod
x0
x1
)
⟶
In
(
proj1
x2
)
x1
(proof)
Theorem
40531..
setprod_mon
:
∀ x0 x1 .
Subq
x0
x1
⟶
∀ x2 x3 .
Subq
x2
x3
⟶
Subq
(
setprod
x0
x2
)
(
setprod
x1
x3
)
(proof)
Theorem
b327e..
setprod_mon0
:
∀ x0 x1 .
Subq
x0
x1
⟶
∀ x2 .
Subq
(
setprod
x0
x2
)
(
setprod
x1
x2
)
(proof)
Theorem
3ea93..
setprod_mon1
:
∀ x0 x1 x2 .
Subq
x1
x2
⟶
Subq
(
setprod
x0
x1
)
(
setprod
x0
x2
)
(proof)
Theorem
98421..
pair_setprod_E0
:
∀ x0 x1 x2 x3 .
In
(
setsum
x2
x3
)
(
setprod
x0
x1
)
⟶
In
x2
x0
(proof)
Theorem
c6ec6..
pair_setprod_E1
:
∀ x0 x1 x2 x3 .
In
(
setsum
x2
x3
)
(
setprod
x0
x1
)
⟶
In
x3
x1
(proof)
Theorem
f9ff3..
lamI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
x0
⟶
∀ x3 .
In
x3
(
x1
x2
)
⟶
In
(
setsum
x2
x3
)
(
lam
x0
x1
)
(proof)
Theorem
e3e5f..
lamE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
(
lam
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
In
x6
(
x1
x4
)
)
(
x2
=
setsum
x4
x6
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
(proof)
Theorem
efa2b..
lamEq
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
iff
(
In
x2
(
lam
x0
x1
)
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
In
x4
x0
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
In
x6
(
x1
x4
)
)
(
x2
=
setsum
x4
x6
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
)
(proof)
Known
043f7..
ap_def
:
ap
=
λ x1 x2 .
ReplSep
x1
(
λ x3 .
∀ x4 : ο .
(
∀ x5 .
x3
=
setsum
x2
x5
⟶
x4
)
⟶
x4
)
proj1
Theorem
970d5..
apI
:
∀ x0 x1 x2 .
In
(
setsum
x1
x2
)
x0
⟶
In
x2
(
ap
x0
x1
)
(proof)
Theorem
0bd41..
apE
:
∀ x0 x1 x2 .
In
x2
(
ap
x0
x1
)
⟶
In
(
setsum
x1
x2
)
x0
(proof)
Theorem
d1a05..
apEq
:
∀ x0 x1 x2 .
iff
(
In
x2
(
ap
x0
x1
)
)
(
In
(
setsum
x1
x2
)
x0
)
(proof)
Theorem
b515a..
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
In
x2
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
(proof)
Known
d0de4..
Empty_eq
:
∀ x0 .
(
∀ x1 .
nIn
x1
x0
)
⟶
x0
=
0
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
Theorem
4862c..
beta0
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
nIn
x2
x0
⟶
ap
(
lam
x0
x1
)
x2
=
0
(proof)