Proof of proveit.logic.sets.inclusion.transitivity_subset_eq_subset_eq theorem

import proveit
from proveit import defaults
from proveit import x, A, B, C
from proveit.logic import InSet, SubsetEq
from proveit.logic.sets.inclusion  import subset_eq_def

%proving transitivity_subset_eq_subset_eq

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

subset_eq_def

 ⊢  

subset_eq_def_inst_AB = subset_eq_def.instantiate({A:A, B:B})

subset_eq_def_inst_AB:  ⊢  

subset_eq_def_inst_BC = subset_eq_def.instantiate({A:B, B:C})

subset_eq_def_inst_BC:  ⊢  

subset_eq_def_inst_AB.derive_right_via_equality(assumptions=[subset_eq_def_inst_AB.lhs])

 ⊢  

subset_eq_def_inst_AB.derive_right_via_equality(assumptions=[subset_eq_def_inst_AB.lhs]).instantiate(
        {x:x}, assumptions=[InSet(x, A), subset_eq_def_inst_AB.lhs])

,  ⊢  

subset_eq_def_inst_BC.derive_right_via_equality(assumptions=[subset_eq_def_inst_BC.lhs]).instantiate(
        assumptions=[InSet(x, A), SubsetEq(A, B), subset_eq_def_inst_BC.lhs])

, ,  ⊢  

subset_eq_def_inst_AC = subset_eq_def.instantiate({A:A, B:C})

subset_eq_def_inst_AC:  ⊢  

subset_eq_def_inst_AC.derive_left_via_equality(assumptions=[SubsetEq(A, B), SubsetEq(B, C)])

,  ⊢  

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

%qed

proveit.logic.sets.inclusion.transitivity_subset_eq_subset_eq has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	,  ⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.lhs_via_equality
3	generalization	5	,  ⊢
4	instantiation	14	⊢
	: , :
5	instantiation	6, 7	, ,  ⊢
	:
6	instantiation	8, 9, 10	⊢
	: , :
7	instantiation	11, 12, 13	,  ⊢
	: , :
8	theorem		⊢
	proveit.logic.equality.rhs_via_equality
9	assumption		⊢
10	instantiation	14	⊢
	: , :
11	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
12	assumption		⊢
13	assumption		⊢
14	axiom		⊢
	proveit.logic.sets.inclusion.subset_eq_def