Search for blocks/addresses/...
Proofgold Address
address
PUMB7D4HDtUirSGdM5YSZAARA9p2rEikmyX
total
0
mg
-
conjpub
-
current assets
9f44d..
/
b6fbc..
bday:
4898
doc published by
Pr6Pc..
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
ordsucc
ordsucc
:
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Theorem
Subq_1_Sing0
Subq_1_Sing0
:
1
⊆
Sing
0
(proof)
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
Subq_Sing0_1
Subq_Sing0_1
:
Sing
0
⊆
1
(proof)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Theorem
eq_1_Sing0
eq_1_Sing0
:
1
=
Sing
0
(proof)
Param
UPair
UPair
:
ι
→
ι
→
ι
Known
UPairI1
UPairI1
:
∀ x0 x1 .
x0
∈
UPair
x0
x1
Known
UPairI2
UPairI2
:
∀ x0 x1 .
x1
∈
UPair
x0
x1
Theorem
Subq_2_UPair01
Subq_2_UPair01
:
2
⊆
UPair
0
1
(proof)
Known
UPairE
UPairE
:
∀ x0 x1 x2 .
x0
∈
UPair
x1
x2
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
Known
In_0_2
In_0_2
:
0
∈
2
Known
In_1_2
In_1_2
:
1
∈
2
Theorem
Subq_UPair01_2
Subq_UPair01_2
:
UPair
0
1
⊆
2
(proof)
Theorem
eq_2_UPair01
eq_2_UPair01
:
2
=
UPair
0
1
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Definition
TransSet
TransSet
:=
λ x0 .
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Definition
ordinal
ordinal
:=
λ x0 .
and
(
TransSet
x0
)
(
∀ x1 .
x1
∈
x0
⟶
TransSet
x1
)
Known
In_ind
In_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
x0
x1
Known
ordinal_Hered
ordinal_Hered
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordinal
x1
Theorem
ordinal_ind
ordinal_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
ordinal
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
ordinal
x1
⟶
x0
x1
(proof)
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Theorem
least_ordinal_ex
least_ordinal_ex
:
∀ x0 :
ι → ο
.
(
∀ x1 : ο .
(
∀ x2 .
and
(
ordinal
x2
)
(
x0
x2
)
⟶
x1
)
⟶
x1
)
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
and
(
ordinal
x2
)
(
x0
x2
)
)
(
∀ x3 .
x3
∈
x2
⟶
not
(
x0
x3
)
)
⟶
x1
)
⟶
x1
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
nat_1
nat_1
:
nat_p
1
Known
ordinal_1
ordinal_1
:
ordinal
1
Known
nat_2
nat_2
:
nat_p
2
Known
ordinal_2
ordinal_2
:
ordinal
2
Param
omega
omega
:
ι
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
nat_p_trans
nat_p_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
nat_p
x1
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
omega_TransSet
omega_TransSet
:
TransSet
omega
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
ordinal_TransSet
ordinal_TransSet
:
∀ x0 .
ordinal
x0
⟶
TransSet
x0
Known
omega_ordinal
omega_ordinal
:
ordinal
omega
Known
ordinal_ordsucc
ordinal_ordsucc
:
∀ x0 .
ordinal
x0
⟶
ordinal
(
ordsucc
x0
)
Known
ordsucc_omega_ordinal
ordsucc_omega_ordinal
:
ordinal
(
ordsucc
omega
)
Known
TransSet_ordsucc_In_Subq
TransSet_ordsucc_In_Subq
:
∀ x0 .
TransSet
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
⊆
x0
Known
ordinal_ordsucc_In_Subq
ordinal_ordsucc_In_Subq
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
⊆
x0
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
or3I1
or3I1
:
∀ x0 x1 x2 : ο .
x0
⟶
or
(
or
x0
x1
)
x2
Known
or3I3
or3I3
:
∀ x0 x1 x2 : ο .
x2
⟶
or
(
or
x0
x1
)
x2
Known
or3I2
or3I2
:
∀ x0 x1 x2 : ο .
x1
⟶
or
(
or
x0
x1
)
x2
Known
or3E
or3E
:
∀ x0 x1 x2 : ο .
or
(
or
x0
x1
)
x2
⟶
∀ x3 : ο .
(
x0
⟶
x3
)
⟶
(
x1
⟶
x3
)
⟶
(
x2
⟶
x3
)
⟶
x3
Known
ordinal_trichotomy_or
ordinal_trichotomy_or
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
or
(
x0
∈
x1
)
(
x0
=
x1
)
)
(
x1
∈
x0
)
Param
exactly1of3
exactly1of3
:
ο
→
ο
→
ο
→
ο
Known
exactly1of3_I1
exactly1of3_I1
:
∀ x0 x1 x2 : ο .
x0
⟶
not
x1
⟶
not
x2
⟶
exactly1of3
x0
x1
x2
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
In_no2cycle
In_no2cycle
:
∀ x0 x1 .
x0
∈
x1
⟶
x1
∈
x0
⟶
False
Known
exactly1of3_I2
exactly1of3_I2
:
∀ x0 x1 x2 : ο .
not
x0
⟶
x1
⟶
not
x2
⟶
exactly1of3
x0
x1
x2
Known
exactly1of3_I3
exactly1of3_I3
:
∀ x0 x1 x2 : ο .
not
x0
⟶
not
x1
⟶
x2
⟶
exactly1of3
x0
x1
x2
Theorem
ordinal_trichotomy
ordinal_trichotomy
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
exactly1of3
(
x0
∈
x1
)
(
x0
=
x1
)
(
x1
∈
x0
)
(proof)
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Known
ordinal_linear
ordinal_linear
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
⊆
x1
)
(
x1
⊆
x0
)
Known
ordinal_ordsucc_In_eq
ordinal_ordsucc_In_eq
:
∀ x0 x1 .
ordinal
x0
⟶
x1
∈
x0
⟶
or
(
ordsucc
x1
∈
x0
)
(
x0
=
ordsucc
x1
)
Known
ordinal_lim_or_succ
ordinal_lim_or_succ
:
∀ x0 .
ordinal
x0
⟶
or
(
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
x0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
x0
)
(
x0
=
ordsucc
x2
)
⟶
x1
)
⟶
x1
)
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
ordinal_ordsucc_In
ordinal_ordsucc_In
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
UnionE_impred
UnionE_impred
:
∀ x0 x1 .
x1
∈
prim3
x0
⟶
∀ x2 : ο .
(
∀ x3 .
x1
∈
x3
⟶
x3
∈
x0
⟶
x2
)
⟶
x2
Known
UnionI
UnionI
:
∀ x0 x1 x2 .
x1
∈
x2
⟶
x2
∈
x0
⟶
x1
∈
prim3
x0
Known
ordinal_Union
ordinal_Union
:
∀ x0 .
(
∀ x1 .
x1
∈
x0
⟶
ordinal
x1
)
⟶
ordinal
(
prim3
x0
)
Param
famunion
famunion
:
ι
→
(
ι
→
ι
) →
ι
Known
famunionE
famunionE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
∈
x1
x4
)
⟶
x3
)
⟶
x3
Known
famunionI
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
x0
⟶
x3
∈
x1
x2
⟶
x3
∈
famunion
x0
x1
Known
ordinal_famunion
ordinal_famunion
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
ordinal
(
x1
x2
)
)
⟶
ordinal
(
famunion
x0
x1
)
Param
binintersect
binintersect
:
ι
→
ι
→
ι
Known
binintersect_Subq_eq_1
binintersect_Subq_eq_1
:
∀ x0 x1 .
x0
⊆
x1
⟶
binintersect
x0
x1
=
x0
Known
binintersect_com
binintersect_com
:
∀ x0 x1 .
binintersect
x0
x1
=
binintersect
x1
x0
Known
ordinal_binintersect
ordinal_binintersect
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
(
binintersect
x0
x1
)
Param
binunion
binunion
:
ι
→
ι
→
ι
Known
Subq_binunion_eq
Subq_binunion_eq
:
∀ x0 x1 .
x0
⊆
x1
=
(
binunion
x0
x1
=
x1
)
Known
binunion_com
binunion_com
:
∀ x0 x1 .
binunion
x0
x1
=
binunion
x1
x0
Known
ordinal_binunion
ordinal_binunion
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
(
binunion
x0
x1
)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
SepE1
SepE1
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x2
∈
x0
Known
ordinal_Sep
ordinal_Sep
:
∀ x0 .
ordinal
x0
⟶
∀ x1 :
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x2
⟶
x1
x2
⟶
x1
x3
)
⟶
ordinal
(
Sep
x0
x1
)
Param
In_rec_i
In_rec_i
:
(
ι
→
(
ι
→
ι
) →
ι
) →
ι
→
ι
Definition
Inj1
Inj1
:=
In_rec_i
(
λ x0 .
λ x1 :
ι → ι
.
binunion
(
Sing
0
)
(
prim5
x0
x1
)
)
Known
In_rec_i_eq
In_rec_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_i
x0
x1
=
x0
x1
(
In_rec_i
x0
)
Known
ReplEq_ext
ReplEq_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
=
prim5
x0
x2
Theorem
Inj1_eq
Inj1_eq
:
∀ x0 .
Inj1
x0
=
binunion
(
Sing
0
)
(
prim5
x0
Inj1
)
(proof)
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Theorem
Inj1I1
Inj1I1
:
∀ x0 .
0
∈
Inj1
x0
(proof)
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
Inj1I2
Inj1I2
:
∀ x0 x1 .
x1
∈
x0
⟶
Inj1
x1
∈
Inj1
x0
(proof)
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
ReplE
ReplE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
x1
x4
)
⟶
x3
)
⟶
x3
Theorem
Inj1E
Inj1E
:
∀ x0 x1 .
x1
∈
Inj1
x0
⟶
or
(
x1
=
0
)
(
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
x1
=
Inj1
x3
)
⟶
x2
)
⟶
x2
)
(proof)
Theorem
Inj1NE1
Inj1NE1
:
∀ x0 .
Inj1
x0
=
0
⟶
∀ x1 : ο .
x1
(proof)
Theorem
Inj1NE2
Inj1NE2
:
∀ x0 .
nIn
(
Inj1
x0
)
(
Sing
0
)
(proof)
Definition
Inj0
Inj0
:=
λ x0 .
prim5
x0
Inj1
Theorem
Inj0I
Inj0I
:
∀ x0 x1 .
x1
∈
x0
⟶
Inj1
x1
∈
Inj0
x0
(proof)
Theorem
Inj0E
Inj0E
:
∀ x0 x1 .
x1
∈
Inj0
x0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
x1
=
Inj1
x3
)
⟶
x2
)
⟶
x2
(proof)
Param
setminus
setminus
:
ι
→
ι
→
ι
Definition
Unj
Unj
:=
In_rec_i
(
λ x0 .
prim5
(
setminus
x0
(
Sing
0
)
)
)
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Theorem
Unj_eq
Unj_eq
:
∀ x0 .
Unj
x0
=
prim5
(
setminus
x0
(
Sing
0
)
)
Unj
(proof)
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
setminusE
setminusE
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
and
(
x2
∈
x0
)
(
nIn
x2
x1
)
Known
exandE_i
exandE_i
:
∀ x0 x1 :
ι → ο
.
(
∀ x2 : ο .
(
∀ x3 .
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 .
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Theorem
Unj_Inj1_eq
Unj_Inj1_eq
:
∀ x0 .
Unj
(
Inj1
x0
)
=
x0
(proof)
Theorem
Inj1_inj
Inj1_inj
:
∀ x0 x1 .
Inj1
x0
=
Inj1
x1
⟶
x0
=
x1
(proof)
Theorem
Unj_Inj0_eq
Unj_Inj0_eq
:
∀ x0 .
Unj
(
Inj0
x0
)
=
x0
(proof)
Theorem
Inj0_inj
Inj0_inj
:
∀ x0 x1 .
Inj0
x0
=
Inj0
x1
⟶
x0
=
x1
(proof)
Known
Repl_Empty
Repl_Empty
:
∀ x0 :
ι → ι
.
prim5
0
x0
=
0
Theorem
Inj0_0
Inj0_0
:
Inj0
0
=
0
(proof)
Known
andER
andER
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x1
Theorem
Inj0_Inj1_neq
Inj0_Inj1_neq
:
∀ x0 x1 .
Inj0
x0
=
Inj1
x1
⟶
∀ x2 : ο .
x2
(proof)
Definition
setsum
setsum
:=
λ x0 x1 .
binunion
(
prim5
x0
Inj0
)
(
prim5
x1
Inj1
)
Theorem
Inj0_setsum
Inj0_setsum
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
Inj0
x2
∈
setsum
x0
x1
(proof)
Theorem
Inj1_setsum
Inj1_setsum
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
Inj1
x2
∈
setsum
x0
x1
(proof)
Theorem
setsum_Inj_inv
setsum_Inj_inv
:
∀ x0 x1 x2 .
x2
∈
setsum
x0
x1
⟶
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
Inj0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x1
)
(
x2
=
Inj1
x4
)
⟶
x3
)
⟶
x3
)
(proof)
Theorem
Inj0_setsum_0L
Inj0_setsum_0L
:
∀ x0 .
setsum
0
x0
=
Inj0
x0
(proof)
Known
In_0_1
In_0_1
:
0
∈
1
Theorem
Inj1_setsum_1L
Inj1_setsum_1L
:
∀ x0 .
setsum
1
x0
=
Inj1
x0
(proof)
Known
nat_complete_ind
nat_complete_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
nat_0_in_ordsucc
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
0
∈
ordsucc
x0
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
nat_inv
nat_inv
:
∀ x0 .
nat_p
x0
⟶
or
(
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
x0
=
ordsucc
x2
)
⟶
x1
)
⟶
x1
)
Known
nat_trans
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Theorem
nat_setsum_ordsucc
nat_setsum1_ordsucc
:
∀ x0 .
nat_p
x0
⟶
setsum
1
x0
=
ordsucc
x0
(proof)
Theorem
setsum_0_0
setsum_0_0
:
setsum
0
0
=
0
(proof)
Known
nat_0
nat_0
:
nat_p
0
Theorem
setsum_1_0_1
setsum_1_0_1
:
setsum
1
0
=
1
(proof)
Theorem
setsum_1_1_2
setsum_1_1_2
:
setsum
1
1
=
2
(proof)
Theorem
pairSubq
pairSubq
:
∀ x0 x1 x2 x3 .
x0
⊆
x2
⟶
x1
⊆
x3
⟶
setsum
x0
x1
⊆
setsum
x2
x3
(proof)
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Definition
combine_funcs
combine_funcs
:=
λ x0 x1 .
λ x2 x3 :
ι → ι
.
λ x4 .
If_i
(
x4
=
Inj0
(
Unj
x4
)
)
(
x2
(
Unj
x4
)
)
(
x3
(
Unj
x4
)
)
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
combine_funcs_eq1
combine_funcs_eq1
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 .
combine_funcs
x0
x1
x2
x3
(
Inj0
x4
)
=
x2
x4
(proof)
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Theorem
combine_funcs_eq2
combine_funcs_eq2
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 .
combine_funcs
x0
x1
x2
x3
(
Inj1
x4
)
=
x3
x4
(proof)
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Definition
proj0
proj0
:=
λ x0 .
ReplSep
x0
(
λ x1 .
∀ x2 : ο .
(
∀ x3 .
Inj0
x3
=
x1
⟶
x2
)
⟶
x2
)
Unj
Definition
proj1
proj1
:=
λ x0 .
ReplSep
x0
(
λ x1 .
∀ x2 : ο .
(
∀ x3 .
Inj1
x3
=
x1
⟶
x2
)
⟶
x2
)
Unj
Theorem
Inj0_pair_0_eq
Inj0_pair_0_eq
:
Inj0
=
setsum
0
(proof)
Theorem
Inj1_pair_1_eq
Inj1_pair_1_eq
:
Inj1
=
setsum
1
(proof)
Theorem
pairI0
pairI0
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
setsum
0
x2
∈
setsum
x0
x1
(proof)
Theorem
pairI1
pairI1
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
setsum
1
x2
∈
setsum
x0
x1
(proof)
Theorem
pairE
pairE
:
∀ x0 x1 x2 .
x2
∈
setsum
x0
x1
⟶
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
setsum
0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x1
)
(
x2
=
setsum
1
x4
)
⟶
x3
)
⟶
x3
)
(proof)
Theorem
pairE0
pairE0
:
∀ x0 x1 x2 .
setsum
0
x2
∈
setsum
x0
x1
⟶
x2
∈
x0
(proof)
Theorem
pairE1
pairE1
:
∀ x0 x1 x2 .
setsum
1
x2
∈
setsum
x0
x1
⟶
x2
∈
x1
(proof)
Param
iff
iff
:
ο
→
ο
→
ο
Known
iffI
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Theorem
pairEq
pairEq
:
∀ x0 x1 x2 .
iff
(
x2
∈
setsum
x0
x1
)
(
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
setsum
0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x1
)
(
x2
=
setsum
1
x4
)
⟶
x3
)
⟶
x3
)
)
(proof)
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Theorem
proj0I
proj0I
:
∀ x0 x1 .
setsum
0
x1
∈
x0
⟶
x1
∈
proj0
x0
(proof)
Known
ReplSepE_impred
ReplSepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
ReplSep
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
x5
∈
x0
⟶
x1
x5
⟶
x3
=
x2
x5
⟶
x4
)
⟶
x4
Theorem
proj0E
proj0E
:
∀ x0 x1 .
x1
∈
proj0
x0
⟶
setsum
0
x1
∈
x0
(proof)
Theorem
proj1I
proj1I
:
∀ x0 x1 .
setsum
1
x1
∈
x0
⟶
x1
∈
proj1
x0
(proof)
Theorem
proj1E
proj1E
:
∀ x0 x1 .
x1
∈
proj1
x0
⟶
setsum
1
x1
∈
x0
(proof)
Theorem
proj0_pair_eq
proj0_pair_eq
:
∀ x0 x1 .
proj0
(
setsum
x0
x1
)
=
x0
(proof)
Theorem
proj1_pair_eq
proj1_pair_eq
:
∀ x0 x1 .
proj1
(
setsum
x0
x1
)
=
x1
(proof)
Theorem
pair_inj
pair_inj
:
∀ x0 x1 x2 x3 .
setsum
x0
x1
=
setsum
x2
x3
⟶
and
(
x0
=
x2
)
(
x1
=
x3
)
(proof)
Theorem
pair_eta_Subq_proj
pair_eta_Subq_proj
:
∀ x0 .
setsum
(
proj0
x0
)
(
proj1
x0
)
⊆
x0
(proof)
previous assets