Theorem Arrow02 | index | src |

theorem Arrow02 (A: set): $ ~A == 0 -> Arrow A 0 == 0 $;
StepHypRefExpression
1 eq0al
Arrow A 0 == 0 <-> A. a1 ~a1 e. Arrow A 0
2 con3
(a1 e. Arrow A 0 -> A == 0) -> ~A == 0 -> ~a1 e. Arrow A 0
3 elArrow
a1 e. Arrow A 0 <-> func a1 A 0
4 func03
func a1 A 0 <-> a1 == 0 /\ A == 0
5 anr
a1 == 0 /\ A == 0 -> A == 0
6 4, 5 sylbi
func a1 A 0 -> A == 0
7 3, 6 sylbi
a1 e. Arrow A 0 -> A == 0
8 2, 7 ax_mp
~A == 0 -> ~a1 e. Arrow A 0
9 8 iald
~A == 0 -> A. a1 ~a1 e. Arrow A 0
10 1, 9 sylibr
~A == 0 -> Arrow A 0 == 0

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)