Proof of proveit.logic.sets.equivalence.set_not_equiv_reversal theorem

import proveit
from proveit import A, B
from proveit.logic import Not, SetNotEquiv
from proveit.logic.sets import SetEquiv
from proveit.logic.sets.equivalence  import set_equiv_def, set_not_equiv_def
from proveit.logic.sets.equivalence import set_equiv_reversal
theory = proveit.Theory() # the theorem's theory

%proving set_not_equiv_reversal

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
set_not_equiv_reversal:
(see dependencies)

set_not_equiv_def

 ⊢  

set_not_equiv_def_inst_AB = set_not_equiv_def.instantiate()

set_not_equiv_def_inst_AB:  ⊢  

set_not_equiv_def_inst_BA = set_not_equiv_def.instantiate({A:B, B:A})

set_not_equiv_def_inst_BA:  ⊢  

set_equiv_reversal

 ⊢  

set_equiv_reversal_inst_BA = set_equiv_reversal.instantiate({A:B, B:A}, assumptions=[SetEquiv(B, A)])

set_equiv_reversal_inst_BA:  ⊢  

set_equiv_reversal_inst_BA_as_implication = set_equiv_reversal_inst_BA.as_implication(hypothesis=SetEquiv(B, A))

set_equiv_reversal_inst_BA_as_implication:  ⊢  

not_AEquivB_gives_not_BEquivA = set_equiv_reversal_inst_BA_as_implication.deny_antecedent(assumptions=[Not(SetEquiv(A, B))])

not_AEquivB_gives_not_BEquivA:  ⊢  

not_AEquivB_gives_not_BEquivA_as_implication = not_AEquivB_gives_not_BEquivA.as_implication(hypothesis=Not(SetEquiv(A, B)))

not_AEquivB_gives_not_BEquivA_as_implication:  ⊢  

c_1 = set_not_equiv_def_inst_AB.sub_left_side_into(not_AEquivB_gives_not_BEquivA_as_implication)

c_1:  ⊢  

c_2 = set_not_equiv_def_inst_BA.sub_left_side_into(c_1)

c_2:  ⊢  

set_not_equiv_reversal may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.logic.sets.equivalence.set_not_equiv_reversal has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	modus ponens	2, 3	⊢
2	instantiation	6, 4, 5	⊢
	: , : , :
3	assumption		⊢
4	instantiation	6, 7, 8	⊢
	: , : , :
5	instantiation	10	⊢
	: , :
6	theorem		⊢
	proveit.logic.equality.sub_left_side_into
7	deduction	9	⊢
8	instantiation	10	⊢
	: , :
9	instantiation	11, 12, 13, 14	⊢
	: , :
10	axiom		⊢
	proveit.logic.sets.equivalence.set_not_equiv_def
11	conjecture		⊢
	proveit.logic.booleans.implication.modus_tollens_denial
12	instantiation	15	⊢
	: , :
13	deduction	16	⊢
14	assumption		⊢
15	conjecture		⊢
	proveit.logic.sets.equivalence.set_equiv_is_bool
16	instantiation	17, 18	⊢
	: , :
17	theorem		⊢
	proveit.logic.sets.equivalence.set_equiv_reversal
18	assumption		⊢