Theorem axbnd
Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical
logic, this and axi12 are fairly straightforward consequences of
axc9. But in intuitionistic logic, it is not easy to add the extra
A. x to axi12 and so we treat the two as separate axioms. Usage of
this theorem is discouraged because it depends on [ax-13]. (Contributed
by Jim Kingdon, 22-Mar-2018.) (Proof shortened by Wolf Lammen,
24-Apr-2023.) (New usage is discouraged.)
Conclusion
\( \vdash \forall z \, z = x \vee (\forall z \, z = y \vee \forall x \, \forall z \, (x = y \rightarrow \forall z \, x = y)) \)
Proof
l0
hbaev
\( \vdash \forall z \, z = x \rightarrow \forall x \, \forall z \, z = x \)
l1
nf5i _
l2
hbaev
\( \vdash \forall z \, z = y \rightarrow \forall x \, \forall z \, z = y \)
l3
nf5i _
l4
nfor l1 _
l5
19.32 l4
\( \vdash \forall x \, (\forall z \, z = x \vee \forall z \, z = y \vee \forall z \, (x = y \rightarrow \forall z \, x = y)) \leftrightarrow \forall z \, z = x \vee \forall z \, z = y \vee \forall x \, \forall z \, (x = y \rightarrow \forall z \, x = y) \)
l6
orass
\( \vdash \forall z \, z = x \vee \forall z \, z = y \vee \forall x \, \forall z \, (x = y \rightarrow \forall z \, x = y) \leftrightarrow \forall z \, z = x \vee (\forall z \, z = y \vee \forall x \, \forall z \, (x = y \rightarrow \forall z \, x = y)) \)
l7
bitri l5 _
\( \vdash \forall x \, (\forall z \, z = x \vee \forall z \, z = y \vee \forall z \, (x = y \rightarrow \forall z \, x = y)) \leftrightarrow \forall z \, z = x \vee (\forall z \, z = y \vee \forall x \, \forall z \, (x = y \rightarrow \forall z \, x = y)) \)
l8
axi12
\( \vdash \forall z \, z = x \vee (\forall z \, z = y \vee \forall z \, (x = y \rightarrow \forall z \, x = y)) \)
l9
orass
\( \vdash \forall z \, z = x \vee \forall z \, z = y \vee \forall z \, (x = y \rightarrow \forall z \, x = y) \leftrightarrow \forall z \, z = x \vee (\forall z \, z = y \vee \forall z \, (x = y \rightarrow \forall z \, x = y)) \)
l10
mpbir l8 _
\( \vdash \forall z \, z = x \vee \forall z \, z = y \vee \forall z \, (x = y \rightarrow \forall z \, x = y) \)
l11
mpgbi l7 _