Require Export tbs_op.

Section Subset_Relative_Operations_Definitions.

   Section relative_membership.
   
      Definition REps: (I,S:Set) S -> (I -> S -> Set) -> Set := [I,S;a;F](LEx I [i](Eps S a (F i))).
   
   End relative_membership.

   Section infinitary_subset_relative_operations.

      Definition SRAll: (I:Set; T:I->Set; S:Set) ((i:I) (T i) -> (S -> Set)) -> (S -> Set) := [I;T;S;R;a](RAll I T [i](REps (T i) S a (R i))).
      
      Definition SREx: (I:Set; T:I->Set; S:Set) ((i:I) (T i) -> (S -> Set)) -> (S -> Set) := [I;T;S;R;a](REx I T [i](REps (T i) S a (R i))).

   End infinitary_subset_relative_operations.

End Subset_Relative_Operations_Definitions.

Section Subset_Relative_Operations_Results.

   Section relative_epsilon_conditions.
   
      Theorem reps_i: (I:Set; i:I; S:Set; a:S; F:I->S->Set) (Eps S a (F i)) -> (REps I S a F).
      Intros.
      Unfold REps.
      MApply '(lex_i I i).
      Qed.
      
      Theorem reps_e: (I,S:Set; a:S; F:I->S->Set; P:Set) ((i:I) (Eps S a (F i)) -> P) -> (REps I S a F) -> P.
      Intros.
      Unfold REps in H0.
      MElim 'H0 'lex_e.
      MApply '(H a0).
      Qed.
      
   End relative_epsilon_conditions.

   Section infinitary_relative_intersection.
   
      Theorem srall_eps_i: (I:Set; T:I->Set; S:Set; a:S; R:(i:I)(T i)->(S->Set)) ((i:I) (REps (T i) S a (R i))) -> (Eps S a (SRAll I T S R)).
      Intros.
      MApply 'eps_i.
      Unfold SRAll.
      MApply 'rall_i.
      MApply '(H a0).
      Qed.
      
      Theorem srall_eps_e: (I:Set; i:I; T:I->Set) (T i) -> (S:Set; a:S; R:(i:I)(T i)->(S->Set)) (Eps S a (SRAll I T S R)) -> (REps (T i) S a (R i)). 
      Intros.
      MCut '(SRAll I T S R a).
      MApply 'eps_e.
      Unfold SRAll in H1.
      MApply '(rall_e I i T).
      MApply 'eps_i.
      Qed.
      
   End infinitary_relative_intersection.

   Section infinitary_relative_union.
   
      Theorem srex_eps_i: (I:Set; i:I; S:Set; a:S; T:I->Set; R:(i:I)(T i)->(S->Set)) (REps (T i) S a (R i)) -> (Eps S a (SREx I T S R)).
      Intros.
      MApply 'eps_i.
      Unfold SREx.
      MApply '(rex_i I i).
      MApply 'eps_i.
      MApply '(reps_e (T i) S a (R i)).
      Qed.
      
      Theorem srex_eps_e: (I:Set; T:I->Set; S:Set; a:S; R:(i:I)(T i)->(S->Set)) (Eps S a (SREx I T S R)) -> (LEx I [i](REps (T i) S a (R i))).
      Intros.
      MCut '(SREx I T S R a).
      MApply 'eps_e.
      Unfold SREx in H0.
      MApply '(rex_e I T [i:I](REps (T i) S a (R i))).
      MApply '(lex_i I a0).
      Qed.

      Theorem srex_sbe: (I:Set; V,W:I->Set; S:Set; F:I->S->Set) (SbE I V W) -> (SbE S (SREx I V S [i;_](F i)) (SREx I W S [i;_](F i))).
      Intros.
      MApply 'sbe_i.
      MCut '(LEx I [i:?](REps (V i) S a [_:?](F i))).
      MApply '(srex_eps_e I V S a [i:?; _:(V i)](F i)).
      MElim 'H1 'lex_e.
      MApply '(srex_eps_i I a0).
      MCut '(W a0).
      MApply 'eps_e.
      MApply '(sbe_e I V).
      MApply 'eps_i.
      MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
      MApply '(reps_i (W a0) H2).
      MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
      Qed.
      
      Theorem srex_sing_e: (S:Set; U:S->Set) (SbE S (SREx S U S [a;_](Sing S a)) U).
      Intros.
      MApply 'sbe_i.
      MCut '(LEx S [b:?](REps (U b) S a [_:?](Sing S b))).
      MApply '(srex_eps_e S U S a [a0:S; _:(U a0)](Sing S a0)).
      MElim 'H0 'lex_e.
      MApply '(reps_e (U a0) S a [_:(U a0)](Sing S a0)).
      MCut '(Id S a0 a).
      MApply 'sing_eps_e.
      MApply '(id_repl S a a0).
      MApply 'eps_i.
      Qed.

      Theorem srex_sing_i: (S:Set; U:S->Set) (SbE S U (SREx S U S [a;_](Sing S a))).
      Intros.
      MApply 'sbe_i.
      MApply '(srex_eps_i S a).
      MCut '(U a).
      MApply 'eps_e.
      MApply '(reps_i (U a) H0).
      MApply 'sing_eps_i.
      Qed.

      Theorem srex_sing: (S:Set; U:S->Set) (SEq S (SREx S U S [a;_](Sing S a)) U).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'srex_sing_e.
      MApply 'srex_sing_i.
      Qed.
      
   End infinitary_relative_union.

End Subset_Relative_Operations_Results.