Primitive
. The name
wsbc
is a term of type
(
(
set
→
prop
)
→
(
(
set
→
prop
)
→
prop
)
)
.
In Proofgold the corresponding term root is
dfea97...
and object id is
a0cd6a...
Primitive
. The name
wceq
is a term of type
(
(
set
→
prop
)
→
(
(
set
→
prop
)
→
prop
)
)
.
In Proofgold the corresponding term root is
eab77d...
and object id is
e1f96c...
(*** $T setmm ***)
(*** $I sig/DefaultElts.mgs ***)
L5
Axiom.
(
ax_mp
) We take the following as an axiom:
(
∀ph :
prop
,
(
∀ps :
prop
,
ph
→
(
wi
ph
ps
)
→
ps
)
)
In Proofgold the corresponding term root is
261f32...
and proposition id is
c627de...
L6
Axiom.
(
ax_frege52c
) We take the following as an axiom:
(
∀ph :
(
set
→
prop
)
,
(
∀A2 :
(
set
→
(
set
→
prop
)
)
,
(
∀B2 :
(
set
→
(
set
→
prop
)
)
,
(
∀x3 :
set
,
(
wi
(
wceq
(
A2
x3
)
(
B2
x3
)
)
(
wi
(
wsbc
(
λx3 :
set
⇒
(
ph
x3
)
)
(
A2
x3
)
)
(
wsbc
(
λx3 :
set
⇒
(
ph
x3
)
)
(
B2
x3
)
)
)
)
)
)
)
)
In Proofgold the corresponding term root is
247a9e...
and proposition id is
f4ba48...
L7
Axiom.
(
ax_frege8
) We take the following as an axiom:
(
∀ph :
prop
,
(
∀ps :
prop
,
(
∀ch :
prop
,
(
wi
(
wi
ph
(
wi
ps
ch
)
)
(
wi
ps
(
wi
ph
ch
)
)
)
)
)
)
In Proofgold the corresponding term root is
a5ffbb...
and proposition id is
545653...
L8
Theorem.
(
frege53c
)
(
∀ph :
(
set
→
prop
)
,
(
∀A2 :
(
set
→
(
set
→
prop
)
)
,
(
∀B2 :
(
set
→
(
set
→
prop
)
)
,
(
∀x3 :
set
,
(
wi
(
wsbc
(
λx3 :
set
⇒
(
ph
x3
)
)
(
A2
x3
)
)
(
wi
(
wceq
(
A2
x3
)
(
B2
x3
)
)
(
wsbc
(
λx3 :
set
⇒
(
ph
x3
)
)
(
B2
x3
)
)
)
)
)
)
)
)
In Proofgold the corresponding term root is
89e42f...
and proposition id is
24ac9f...
Proof:
Load proof
Proof not loaded.