(** This module (Toolbox - subsets: operations) defines:
    - subset binary intersection:     [SAnd] (subset and)
    - subset binary union:            [SOr]  (subset or)
    - subset implication:             [SImp] (subset implies) 
    - subset opposite:                [SNot] (subset not) 
    - subset infinitary intersection: [SAll] (subset all)
    - subset infinitary union:        [SEx]  (subset exists)
    
    and provides:
    - introduction and elimination rules for the defined constants
    - standard properties (idempotency, commutativity, associativity, compatibility, distributivity) for the defined constants
    - Cantor's diagonalization theorem: [cantor_diag]
    
% \hrule %
 
 We require Toolbox relations and the underlying theory.
  
 *)
Require Export tbs_rel.

Section Subset_Operations_Definitions.

   Section finitary_subset_operations.

(** Subset and: [(SAnd S U V)] corresponds to $ U \sand_S V $. *)
      Definition SAnd: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
      Intros S U V a.
      Exact (LAnd (U a) (V a)).
      Defined.

(** Subset or: [(SOr S U V)] corresponds to $ U \sor_S V $. *)
      Definition SOr: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
      Intros S U V a.
      Exact (LOr (U a) (V a)).
      Defined.
   
(** Subset implies: [(SImp S U V)] corresponds to $ U \simp_S V $. *)
      Definition SImp: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
      Intros S U V a.
      Exact (U a)->(V a).
      Defined.

(** Subset not: [(SNot S U)] corresponds to $ \snot_S U $. *)
      Definition SNot: (S:Set) (S -> Set) -> (S -> Set).
      Intros S U a.
      Exact (LNot (U a)).
      Defined.

   End finitary_subset_operations.
   
   Section infinitary_subset_operations.

(** Subset all: [(SAll I S F)] corresponds to $ \bigsand_S\subset{F(i) \st i \in I} $. *)
      Definition SAll: (I,S:Set) (I -> S -> Set) -> (S -> Set).
      Intros I S F a.
      Exact (i:I)(F i a).
      Defined.

(** Subset exists: [(SEx I S F)] corresponds to $ \bigsor_S\subset{F(i) \st i \in I} $. *)
      Definition SEx: (I,S:Set) (I -> S -> Set) -> (S -> Set).
      Intros I S F a.
      Exact (LEx I [i](F i a)).
      Defined.

   End infinitary_subset_operations.

End Subset_Operations_Definitions.

Section Subset_Operations_Results.

   Section subset_binary_intersection.

(** Subset and, epsilon introduction: $ a \e U \limp a \e V \limp a \e U \sand V $. *)
      Theorem sand_eps_i: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a V) -> (Eps S a (SAnd S U V)).
      Intros.
      MApply 'eps_i.
      Unfold SAnd.
      MApply 'land_i.
      MApply 'eps_e.
      MApply 'eps_e.      
      Qed.

(** Subset and, epsilon elimination 2: $ a \e U \sand V \limp a \e U $. *)
      Theorem sand_eps_e2: (S:Set; V,U:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a U).
      Intros.
      MApply 'eps_i.
      MApply '(land_e2 (V a)).
      Fold (SAnd S U V a).
      MApply 'eps_e.
      Qed.

(** Subset and, epsilon elimination 1: $ a \e U \sand V \limp a \e V $. *)
      Theorem sand_eps_e1: (S:Set; U,V:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a V).
      Intros.
      MApply 'eps_i.
      MApply '(land_e1 (U a)).
      Fold (SAnd S U V a).
      MApply 'eps_e.
      Qed.

(** Subset and, epsilon criterion: $ a \e U \land a \e V \liff a \e U \sand V $ *)
      Theorem sand_eps: (S:Set; U,V:S->Set; a:S) (LIff (LAnd (Eps S a U) (Eps S a V)) (Eps S a (SAnd S U V))).
      Intros.
      MApply 'liff_i.
      MApply 'sand_eps_i.
      MApply '(land_e2 (Eps S a V)).
      MApply '(land_e1 (Eps S a U)).
      MApply 'land_i.
      MApply '(sand_eps_e2 S V).
      MApply '(sand_eps_e1 S U).
      Qed.

(** Subset and, sub or equal elimination 2: $ U \sand V \sub U $. *)
      Theorem sand_sbe_e2: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) U).
      Intros.
      MApply 'sbe_i.
      MApply '(sand_eps_e2 S V).
      Qed.

(** Subset and, sub or equal elimination 1: $ U \sand V \sub V $. *)
      Theorem sand_sbe_e1: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) V).
      Intros.
      MApply 'sbe_i.
      MApply '(sand_eps_e1 S U).
      Qed.

(** Subset and, sub or equal introduction: $ W \sub U \limp W \sub V \limp W \sub U \sand V $. *)
      Theorem sand_sbe_i: (S:Set; W,U,V:S->Set) (SbE S W U) -> (SbE S W V) -> (SbE S W (SAnd S U V)).
      Intros.
      MApply 'sbe_i.
      MApply 'sand_eps_i.
      MApply '(sbe_e S W).
      MApply '(sbe_e S W).
      Qed.

(** Subset and, sub or equal compatibility 2: $ U \sub V \limp U \sand W \sub V \sand W $. *)
      Theorem sand_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S U W) (SAnd S V W)).
      Intros.
      MApply 'sand_sbe_i.
      MApply '(sbe_t S U).
      MApply 'sand_sbe_e2.
      MApply 'sand_sbe_e1.
      Qed.

(** Subset and, sub or equal subset top: $ U \sub \stop \sand U $. *)
      Theorem sand_sbe_stop: (S:Set; U:S->Set) (SbE S U (SAnd S (STop S) U)).
      Intros.
      MApply 'sand_sbe_i.
      MApply 'stop_sbe_i.
      MApply 'sbe_r.
      Qed.

(** Subset and, sub or equal idempotency: $ U \sub U \sand U $. *)
      Theorem sand_sbe_r: (S:Set; U:S->Set) (SbE S U (SAnd S U U)).
      Intros.
      MApply 'sand_sbe_i.
      MApply 'sbe_r.
      MApply 'sbe_r.
      Qed.

(** Subset and, idempotency $ U \sand U = U $. *)
      Theorem sand_r: (S:Set; U:S->Set) (SEq S (SAnd S U U) U).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sand_sbe_e2.
      MApply 'sand_sbe_r.
      Qed.

(** Subset and, sub or equal commutativity: $ V \sand U \sub U \sand V $. *)
      Theorem sand_sbe_s: (S:Set; U,V:S->Set) (SbE S (SAnd S V U) (SAnd S U V)).
      Intros.
      MApply 'sand_sbe_i.
      MApply 'sand_sbe_e1.
      MApply 'sand_sbe_e2.
      Qed.

(** Subset and, commutativity: $ V \sand U = U \sand V $. *)
      Theorem sand_s: (S:Set; U,V:S->Set) (SEq S (SAnd S V U) (SAnd S U V)).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sand_sbe_s.
      MApply 'sand_sbe_s.
      Qed.

(** Subset and, sub or equal associativity 1: $ U \sand (V \sand W) \sub (U \sand V) \sand W $. *)
      Theorem sand_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
      Intros.
      MApply 'sand_sbe_i.
      MApply 'sand_sbe_i.
      MApply 'sand_sbe_e2.
      MApply '(sbe_t S (SAnd S V W)).
      MApply 'sand_sbe_e1.
      MApply 'sand_sbe_e2.
      MApply '(sbe_t S (SAnd S V W)).
      MApply 'sand_sbe_e1.
      MApply 'sand_sbe_e1.
      Qed.

(** Subset and, sub or equal associativity 2: $ (U \sand V) \sand W \sub U \sand (V \sand W) $. *)
      Theorem sand_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SAnd S (SAnd S U V) W) (SAnd S U (SAnd S V W))).
      Intros.
      MApply '(sbe_t S (SAnd S W (SAnd S U V))).
      MApply 'sand_sbe_s.
      MApply '(sbe_t S (SAnd S (SAnd S V W) U)).
      MApply '(sbe_t S (SAnd S (SAnd S W U) V)).
      MApply 'sand_sbe_a1.
      MApply '(sbe_t S (SAnd S V (SAnd S W U))).
      MApply 'sand_sbe_s.
      MApply 'sand_sbe_a1.
      MApply 'sand_sbe_s.
      Qed.

(** Subset and, associativity: $ U \sand (V \sand W) = (U \sand V) \sand W $. *)
      Theorem sand_a: (S:Set; U,V,W:S->Set) (SEq S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sand_sbe_a1.
      MApply 'sand_sbe_a2.
      Qed.

(** Subset and, sub or equal compatibility 1: $ U \sub V \limp W \sand U \sub W \sand V $. *)
      Theorem sand_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S W U) (SAnd S W V)).
      Intros.
      MApply '(sbe_t S (SAnd S U W)).
      MApply 'sand_sbe_s.
      MApply '(sbe_t S (SAnd S V W)).
      MApply 'sand_sbe_c2.
      MApply 'sand_sbe_s.
      Qed.

(** Subset and, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sand W \sub V \sand X $. *)
      Theorem sand_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SAnd S U W) (SAnd S V X)).
      Intros.
      MApply '(sbe_t S (SAnd S V W)).
      MApply 'sand_sbe_c2.
      MApply 'sand_sbe_c1.
      Qed.

   End subset_binary_intersection.
   
   Section subset_binary_union.

(** Subset or, epsilon introduction 2: $ a \e U \limp a \e U \sor V $. *)
      Theorem sor_eps_i2: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a (SOr S U V)).
      Intros.
      MApply 'eps_i.
      Unfold SOr.
      MApply 'in_l.
      MApply 'eps_e.      
      Qed.

(** Subset or, epsilon introduction 1: $ a \e V \limp a \e U \sor V $. *)
      Theorem sor_eps_i1: (S:Set; U,V:S->Set; a:S) (Eps S a V) -> (Eps S a (SOr S U V)).
      Intros.
      MApply 'eps_i.
      Unfold SOr.
      MApply 'in_r.
      MApply 'eps_e.      
      Qed.

(** Subset or, epsilon elimination: $ (a \e U \limp T) \limp (a \e V \limp T) \limp a \e U \sor V \limp T $. *)
      Theorem sor_eps_e: (S:Set; a:S; U,V:S->Set; T:Set) ((Eps S a U) -> T) -> ((Eps S a V) -> T) -> (Eps S a (SOr S U V)) -> T.
      Intros.
      MCut '(SOr S U V a).
      MApply 'eps_e.
      MApply '(lor_e (U a) (V a)).
      MApply 'H.
      MApply 'eps_i.
      MApply 'H0.
      MApply 'eps_i.
      Qed.

(** Subset or, epsilon criterion: $ a \e U \lor a \e V \liff a \e U \sor V $. *)
      Theorem sor_eps: (S:Set; U,V:S->Set; a:S) (LIff (LOr (Eps S a U) (Eps S a V)) (Eps S a (SOr S U V))).
      Intros.
      MApply 'liff_i.
      MApply '(lor_e (Eps S a U) (Eps S a V)).
      MApply 'sor_eps_i2.
      MApply 'sor_eps_i1.
      MApply '(sor_eps_e S a U V).
      MApply 'in_l.
      MApply 'in_r.
      Qed.

(** Subset or, sub or equal introduction 2: $ U \sub U \sor V $. *)
      Theorem sor_sbe_i2: (S:Set; U,V:S->Set) (SbE S U (SOr S U V)).
      Intros.
      MApply 'sbe_i.
      MApply 'sor_eps_i2.
      Qed.

(** Subset or, sub or equal introduction 1: $ V \sub U \sor V $. *)
      Theorem sor_sbe_i1: (S:Set; U,V:S->Set) (SbE S V (SOr S U V)).
      Intros.
      MApply 'sbe_i.
      MApply 'sor_eps_i1.
      Qed.

(** Subset or, sub or equal elimination: $ U \sub W \limp V \sub W \limp U \sor V \sub W $. *)
      Theorem sor_sbe_e: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S V W) -> (SbE S (SOr S U V) W).
      Intros.
      MApply 'sbe_i.
      MApply '(sor_eps_e S a U V).
      MApply '(sbe_e S U).
      MApply '(sbe_e S V).
      Qed.

(** Subset or, sub or equal compatibility 2: $ U \sub V \limp U \sor W \sub V \sor W $. *)
      Theorem sor_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S U W) (SOr S V W)).
      Intros.
      MApply 'sor_sbe_e.
      MApply '(sbe_t S V).
      MApply 'sor_sbe_i2.
      MApply 'sor_sbe_i1.
      Qed.

(** Subset or, sub or equal idempotency: $ U \sor U \sub U $. *)
      Theorem sor_sbe_r: (S:Set; U:S->Set) (SbE S (SOr S U U) U).
      Intros.
      MApply 'sor_sbe_e.
      MApply 'sbe_r.
      MApply 'sbe_r.
      Qed.

(** Subset or, idempotency: $ U \sor U = U $. *)
      Theorem sor_r: (S:Set; U:S->Set) (SEq S (SOr S U U) U).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sor_sbe_r.
      MApply 'sor_sbe_i2.
      Qed.

(** Subset or, sub or equal commutativity: $ V \sor U \sub U \sor V $. *)
      Theorem sor_sbe_s: (S:Set; U,V:S->Set) (SbE S (SOr S V U) (SOr S U V)).
      Intros.
      MApply 'sor_sbe_e.
      MApply 'sor_sbe_i1.
      MApply 'sor_sbe_i2.      
      Qed.

(** Subset or, commutativity: $ V \sor U = U \sor V $. *)
      Theorem sor_s: (S:Set; U,V:S->Set) (SEq S (SOr S V U) (SOr S U V)).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sor_sbe_s.
      MApply 'sor_sbe_s.
      Qed.

(** Subset or, sub or equal associativity 1: $ U \sor (V \sor W) \sub (U \sor V) \sor W $. *)
      Theorem sor_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
      Intros.
      MApply 'sor_sbe_e.
      MApply '(sbe_t S (SOr S U V)).
      MApply 'sor_sbe_i2.
      MApply 'sor_sbe_i2.
      MApply 'sor_sbe_e.
      MApply '(sbe_t S (SOr S U V)).
      MApply 'sor_sbe_i1.
      MApply 'sor_sbe_i2.
      MApply 'sor_sbe_i1.
      Qed.

(** Subset or, sub or equal associativity 2: $ (U \sor V) \sor W \sub U \sor (V \sor W) $. *)
      Theorem sor_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SOr S (SOr S U V) W) (SOr S U (SOr S V W))).
      Intros.
      MApply '(sbe_t S (SOr S W (SOr S U V))).
      MApply 'sor_sbe_s.
      MApply '(sbe_t S (SOr S (SOr S V W) U)).
      MApply '(sbe_t S (SOr S (SOr S W U) V)).
      MApply 'sor_sbe_a1.
      MApply '(sbe_t S (SOr S V (SOr S W U))).
      MApply 'sor_sbe_s.
      MApply 'sor_sbe_a1.
      MApply 'sor_sbe_s.
      Qed.

(** Subset or, associativity: $ U \sor (V \sor W) = (U \sor V) \sor W $. *)
      Theorem sor_a: (S:Set; U,V,W:S->Set) (SEq S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sor_sbe_a1.
      MApply 'sor_sbe_a2.
      Qed.

(** Subset or, sub or equal compatibility 1: $ U \sub V \limp W \sor U \sub W \sor V $. *)
      Theorem sor_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S W U) (SOr S W V)).
      Intros.
      MApply '(sbe_t S (SOr S U W)).
      MApply 'sor_sbe_s.
      MApply '(sbe_t S (SOr S V W)).
      MApply 'sor_sbe_c2.
      MApply 'sor_sbe_s.
      Qed.

(** Subset or, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sor W \sub V \sor X $. *)
      Theorem sor_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SOr S U W) (SOr S V X)).
      Intros.
      MApply '(sbe_t S (SOr S V W)).
      MApply 'sor_sbe_c2.
      MApply 'sor_sbe_c1.
      Qed.

   End subset_binary_union.
   
   Section subset_implication.

(** Subset implies, epsilon introduction: $ (a \e U \limp a \e V) \limp a \e U \simp V $. *)
      Theorem simp_eps_i: (S:Set; U,V:S->Set; a:S) ((Eps S a U) -> (Eps S a V)) -> (Eps S a (SImp S U V)).
      Intros.
      MApply 'eps_i.
      Unfold SImp.
      Intros.
      MApply 'eps_e.
      MApply 'H.
      MApply 'eps_i.
      Qed.

(** Subset implies, epsilon elimination: $ a \e U \simp V \limp a \e U \limp a \e V $. *)
      Theorem simp_eps_e: (S:Set; U,V:S->Set; a:S) (Eps S a (SImp S U V)) -> (Eps S a U) -> (Eps S a V).
      Intros.
      MApply 'eps_i.
      Apply (mcut (U a)).
      MApply 'eps_e.
      MApply '(eps_e S a).
      Qed.

(** Subset implies, epsilon criterion: $ a \e U \simp V \liff (a \e U \limp a \e V) $. *)
      Theorem simp_eps: (S:Set; U,V:S->Set; a:S) (LIff (Eps S a (SImp S U V)) (Eps S a U) -> (Eps S a V)).
      Intros.
      MApply 'liff_i.
      MApply '(simp_eps_e S U).
      MApply 'simp_eps_i.
      MApply 'H.
      Qed.

(** Subset implies, sub or equal elimination: $ W \sub U \simp V \limp W \sand U \sub V $. *)
      Theorem simp_sbe_e: (S:Set; U,V,W:S->Set) (SbE S W (SImp S U V)) -> (SbE S (SAnd S W U) V).
      Intros.
      MApply 'sbe_i.
      MApply '(simp_eps_e S U).
      MApply '(sbe_e S W).
      MApply '(sand_eps_e2 S U).
      MApply '(sand_eps_e1 S W).
      Qed.

(** Subset implies, sub or equal introduction: $ W \sand U \sub V \limp W \sub U \simp V $. *)
      Theorem simp_sbe_i: (S:Set; U,V,W:S->Set) (SbE S (SAnd S W U) V) -> (SbE S W (SImp S U V)).
      Intros.
      MApply 'sbe_i.
      MApply 'simp_eps_i.
      MApply '(sbe_e S (SAnd S W U)).
      MApply 'sand_eps_i.
      Qed.

(** Subset implies, sub or equal compatibility 2: $ V \sub U \limp U \simp W \sub V \simp W $. *)
      Theorem simp_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S V U) -> (SbE S (SImp S U W) (SImp S V W)).
      Intros.
      MApply 'simp_sbe_i.
      MApply '(sbe_t S (SAnd S (SImp S U W) U)).
      MApply 'sand_sbe_c1.
      MApply 'simp_sbe_e.
      MApply 'sbe_r.
      Qed.

(** Subset implies, sub or equal compatibility 2: $ U \sub V \limp W \simp U \sub W \simp V $. *)
      Theorem simp_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SImp S W U) (SImp S W V)).
      Intros.
      MApply 'simp_sbe_i.
      MApply '(sbe_t S U).
      MApply 'simp_sbe_e.
      MApply 'sbe_r.
      Qed.

(** Subset implies, subset top elimination: $ \stop \sub U \simp V \limp U \sub V $. *)
      Theorem simp_stop_e: (S:Set; U,V:S->Set) (SbE S (STop S) (SImp S U V)) -> (SbE S U V).
      Intros.
      MApply '(sbe_t S (SAnd S (STop S) U)).
      MApply 'sand_sbe_stop.
      MApply 'simp_sbe_e.
      Qed.

(** Subset implies, subset top introduction: $ U \sub V \limp \stop \sub U \simp V $. *)
      Theorem simp_stop_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S (STop S) (SImp S U V)). 
      Intros.
      MApply 'simp_sbe_i.
      MApply '(sbe_t S U).
      MApply 'sand_sbe_e1.
      Qed.

(** Subset implies, subset top criterion: $ \stop \sub U \simp V \liff U \sub V $. *)
      Theorem simp_stop: (S:Set; U,V:S->Set) (LIff (SbE S (STop S) (SImp S U V)) (SbE S U V)).
      Intros.
      MApply 'liff_i.
      MApply 'simp_stop_e.
      MApply 'simp_stop_i.
      Qed.

   End subset_implication.
   
   Section subset_negation.

(** Subset not, epsilon introduction: $ \lnot (a \e U) \limp a \e \snot U $. *)
      Theorem snot_eps_i: (S:Set; U:S->Set; a:S) (LNot (Eps S a U)) -> (Eps S a (SNot S U)).
      Intros.
      MApply 'eps_i.
      Unfold SNot.
      MApply 'lnot_i.
      MApply '(lnot_e (Eps S a U)).
      MApply 'eps_i.
      Qed.

(** Subset not, epsilon elimination: $ a \e \snot U \limp \lnot (a \e U) $. *)
      Theorem snot_eps_e: (S:Set; U:S->Set; a:S) (Eps S a (SNot S U)) -> (LNot (Eps S a U)).
      Unfold SNot.
      Intros.
      MApply 'lnot_i.
      MApply '(lnot_e (U a)).
      MApply '(eps_e S a [a0:S](LNot (U a0))).
      MApply 'eps_e.
      Qed.

(** Subset not, epsilon criterion: $ \lnot (a \e U) \liff a \e \snot U $. *)
      Theorem snot_eps: (S:Set; U:S->Set; a:S) (LIff (LNot (Eps S a U)) (Eps S a (SNot S U))).
      Intros.
      MApply 'liff_i.
      MApply 'snot_eps_i.
      MApply 'snot_eps_e.
      Qed.

(** Subset not, subset implication compatibility: $ \snot U = U \simp \sbot $. *)
      Theorem snot_simp_c: (S:Set; U:S->Set) (SEq S (SNot S U) (SImp S U (SBot S))).
      Intros.
      MApply 'seq_i.
      MApply 'simp_eps_i.
      MCut 'Empty.
      MApply '(lnot_e (Eps S a U)).
      MApply 'snot_eps_e.
      MElim 'H1 'efq.
      MApply 'snot_eps_i.
      MApply 'lnot_i.
      MApply '(sbot_eps_e S a).
      MApply '(simp_eps_e S U).
      Qed.

   End subset_negation.

   Section subset_infinitary_intersection.

(** Subset all, epsilon introduction: $ ((\lall i \in I)\ a \e F(i)) \limp a \e \bigsand\subset{F(i) \st i \in I} $. *)
      Theorem sall_eps_i: (I,S:Set; F:(I->S->Set); a:S) ((i:I) (Eps S a (F i))) -> (Eps S a (SAll I S F)).
      Intros.
      MApply 'eps_i.
      Unfold SAll.
      Intros.
      MApply 'eps_e.
      MApply '(H i).
      Qed.

(** Subset all, epsilon elimination: $ a \e \bigsand\subset{F(i) \st i \in I} \limp (\lall i \in I)\ a \e F(i) $. *)
      Theorem sall_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SAll I S F)) -> (i:I) (Eps S a (F i)).
      Intros.
      MApply 'eps_i.
      Apply (mcut (i:I)(F i a)).
      MApply '(eps_e S a).
      Intros.
      MApply '(H0 i).
      Qed.

(** Subset all, epsilon criterion: $ a \e \bigsand\subset{F(i) \st i \in I} \liff (\lall i \in I)\ a \e F(i) $. *)
      Theorem sall_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SAll I S F)) (i:I) (Eps S a (F i))).
      Intros.
      MApply 'liff_i.
      MApply '(sall_eps_e I).
      MApply 'sall_eps_i.
      MApply '(H i).
      Qed.

(** Subset all, sub or equal elimination: $ (\lall i \in I)\ \bigsand\subset{F(i) \st i \in I} \sub F(i) $. *)
      Theorem sall_sbe_e: (I,S:Set; F:(I->S->Set); i:I) (SbE S (SAll I S F) (F i)). 
      Intros.
      MApply 'sbe_i.
      MApply '(sall_eps_e I).
      Qed.

(** Subset all, sub or equal introduction: $ ((\lall i \in I)\ W \sub F(i)) \limp W \sub \bigsand\subset{F(i) \st i \in I} $. *)
      Theorem sall_sbe_i: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S W (F i))) -> (SbE S W (SAll I S F)).
      Intros.
      MApply 'sbe_i.
      MApply 'sall_eps_i.
      MApply '(sbe_e S W).
      MApply 'H.
      Qed.
      
   End subset_infinitary_intersection.

   Section subset_infinitary_union.

(** Subset exists, epsilon introduction: $ ((\lex i \in I)\ a \e F(i)) \limp a \e \bigsor\subset{F(i) \st i \in I} $. *)
      Theorem sex_eps_i: (I,S:Set; F:(I->S->Set); a:S) (LEx I [i](Eps S a (F i))) -> (Eps S a (SEx I S F)).
      Intros.
      MApply 'eps_i.
      Unfold SEx.
      MElim 'H 'lex_e.
      MApply '(lex_i I a0).
      MApply 'eps_e.
      Qed.

(** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \limp (\lex i \in I)\ a \e F(i) $. *)
      Theorem sex_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SEx I S F)) -> (LEx I [i](Eps S a (F i))).
      Intros.
      MCut '(SEx I S F a).
      MApply 'eps_e.
      MElim 'H0 'lex_e.
      MApply '(lex_i I a0).
      MApply 'eps_i.
      Qed.

(** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \liff (\lex i \in I)\ a \e F(i) $. *)
      Theorem sex_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SEx I S F)) (LEx I [i](Eps S a (F i)))).
      Intros.
      MApply 'liff_i.
      MApply 'sex_eps_e.
      MApply 'sex_eps_i.
      Qed.

(** Subset exists, sub or equal introduction: $ (\lall i \in I)\ F(i) \sub \bigsor\subset{F(i) \st i \in I} $. *)
      Theorem sex_sbe_i: (I,S:Set; F:(I->S->Set); i:I) (SbE S (F i) (SEx I S F)). 
      Intros.
      MApply 'sbe_i.
      MApply 'sex_eps_i.
      MApply '(lex_i I i).
      Qed.

(** Subset exists, sub or equal elimination: $ ((\lall i \in I)\ F(i) \sub W) \limp \bigsor\subset{F(i) \st i \in I} \sub W $. *)
      Theorem sex_sbe_e: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S (F i) W)) -> (SbE S (SEx I S F) W).
      Intros.
      MApply 'sbe_i.
      MCut '(LEx I [i:I](Eps S a (F i))).
      MApply 'sex_eps_e.
      MElim 'H1 'lex_e.
      MApply '(sbe_e S (F a0)).
      MApply 'H.
      Qed.
      
   End subset_infinitary_union.

   Section subset_frame.

(** Frame, subset and introduction: $ U \sub V \limp U \sand V = U $. *)
      Theorem frame_sand_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SAnd S U V) U).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'sand_sbe_e2.
      MApply '(sbe_t S (SAnd S U U)).
      MApply 'sand_sbe_r.
      MApply 'sand_sbe_c1.
      Qed.

(** Frame, subset and elimination: $ U \sand V = U \limp U \sub V $. *)
      Theorem frame_sand_e: (S:Set; U,V:S->Set) (SEq S (SAnd S U V) U) -> (SbE S U V).
      Intros.
      MApply '(sbe_t S (SAnd S U V)).
      MApply '(land_e1 (SbE S (SAnd S U V) U)).
      MApply 'seq_sbe_e.
      MApply 'sand_sbe_e1.
      Qed.

(** Frame, subset or introduction: $ U \sub V \limp U \sor V = V $. *)
      Theorem frame_sor_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SOr S U V) V).
      Intros.
      MApply 'seq_sbe_i.
      MApply '(sbe_t S (SOr S V V)).
      MApply 'sor_sbe_c2.
      MApply 'sor_sbe_r.
      MApply 'sor_sbe_i1.
      Qed.

(** Frame, subset or elimination: $ U \sor V = V \limp U \sub V $. *)
      Theorem frame_sor_e: (S:Set; U,V:S->Set) (SEq S (SOr S U V) V) -> (SbE S U V).
      Intros.
      MApply '(sbe_t S (SOr S U V)).
      MApply 'sor_sbe_i2.      
      MApply '(land_e2 (SbE S V (SOr S U V))).
      MApply 'seq_sbe_e.
      Qed.

(** Frame, subset exists introduction: $ \bigsor\subset{F(i) \st i \in I} \sand W \sub \bigsor\subset{F(i) \sand W \st i \in I} $. *)
      Theorem frame_sex_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
      Intros.
      MApply 'sbe_i.
      MApply 'sex_eps_i.
      MCut '(Eps S a (SEx I S F)).
      MApply '(sand_eps_e2 S W).
      MCut '(LEx I [i:I](Eps S a (F i))).
      MApply 'sex_eps_e.
      MElim 'H1 'lex_e.
      MApply '(lex_i I a0).
      MApply 'sand_eps_i.
      MApply '(sand_eps_e1 S (SEx I S F)).
      Qed.

(** Frame, subset exists elimination: $ \bigsor\subset{F(i) \sand W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \sand W $. *)
      Theorem frame_sex_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SEx I S [i]
(SAnd S (F i) W)) (SAnd S (SEx I S F) W)).
      Intros.
      MApply 'sand_sbe_i.
      MApply 'sex_sbe_e.
      MApply '(sbe_t S (F i)).
      MApply 'sand_sbe_e2.
      MApply 'sex_sbe_i.
      MApply 'sex_sbe_e.
      MApply 'sand_sbe_e1.
      Qed.

(** Frame, subset exists distributivity: $ \bigsor\subset{F(i) \st i \in I} \sand W = \bigsor\subset{F(i) \sand W \st i \in I} $. *)
      Theorem frame_sex_d: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'frame_sex_i.
      MApply 'frame_sex_e.
      Qed.

(** Frame, subset implies elimination: $ \bigsor\subset{F(i) \st i \in I} \simp W \sub \bigsand\subset{F(i) \simp W \st i \in I} $. *)
      Theorem frame_simp_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
      Intros.
      MApply 'sall_sbe_i.
      MApply 'simp_sbe_c2.
      MApply 'sex_sbe_i.
      Qed.

(** Frame, subset implies introduction: $ \bigsand\subset{F(i) \simp W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \simp W $. *)
      Theorem frame_simp_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAll I S [i](SImp S (F i) W)) (SImp S (SEx I S F) W)).
      Intros.
      MApply 'sbe_i.
      MApply 'simp_eps_i.
      MCut '(LEx I [i:I](Eps S a (F i))).
      MApply 'sex_eps_e.
      MElim 'H1 'lex_e.
      MApply '(simp_eps_e S (F a0)).
      MApply '(sall_eps_e I S [i:I](SImp S (F i) W)).
      Qed.

(** Frame, subset implies compatibility: $ \bigsor\subset{F(i) \st i \in I} \simp W = \bigsand\subset{F(i) \simp W \st i \in I} $. *)
      Theorem frame_simp_c: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'frame_simp_e.
      MApply 'frame_simp_i.
      Qed.
      
   End subset_frame.

   Section cantor_diagonalization.

(** [(D S F)] is Cantor's subset $ D_F $. *)
      Local D: (S:Set) (S -> S -> Set) -> (S -> Set).
      Intros S F.
      Exact (SNot S [a:S](F a a)).
      Defined.

(** Cantor's diagonalization: $ (\lall b \in S)\ \lnot (F(b) = D_F) $. *)
      Theorem cantor_diag: (S:Set; F:S->S->Set) (b:S) (LNot (SEq S (F b) (D S F))).
      Intros.
      MApply 'lnot_i.   
      MCut '(LIff (Eps S b (F b)) (LNot (Eps S b (F b)))).
      MApply 'liff_i.
      MApply 'snot_eps_e.
      Change (Eps S b (D S F)).
      MApply '(seq_e1 S (F b)).
      MApply '(seq_e2 S (D S F)).
      Change (Eps S b (SNot S (F b))).
      MApply 'snot_eps_i.
      MApply '(lnot_liff_lbot (Eps S b (F b))).
      Qed.
   
   End cantor_diagonalization.

End Subset_Operations_Results.