Theory pred_set

⊢ ∀P. BIGINTER P = {x | ∀s. s ∈ P ⇒ x ∈ s}

⊢ ∀P. BIGUNION P = {x | ∃s. s ∈ P ∧ x ∈ s}

⊢ ∀f s t. BIJ f s t ⇔ INJ f s t ∧ SURJ f s t

⊢ CARD ∅ = 0 ∧
  ∀s. FINITE s ⇒
      ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

⊢ ∀s. s ≠ ∅ ⇒ CHOICE s ∈ s

⊢ ∀P. COMPL P = 𝕌(:α) DIFF P

⊢ ∀P Q. P × Q = {p | FST p ∈ P ∧ SND p ∈ Q}

⊢ ∀s x. s DELETE x = s DIFF {x}

⊢ ∀P Q. DFUNSET P Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q x)

⊢ ∀s t. s DIFF t = {x | x ∈ s ∧ x ∉ t}

⊢ ∀s t. DISJOINT s t ⇔ s ∩ t = ∅

⊢ ∅ = (λx. F)

⊢ ∀s. FINITE s ⇔ ∀P. P ∅ ∧ (∀s. P s ⇒ ∀e. P (e INSERT s)) ⇒ P s

⊢ ∀P Q. FUNSET P Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q)

⊢ ∀f v. v ∈ GSPEC f ⇔ ∃x. (v,T) = f x

⊢ ∀s n. s HAS_SIZE n ⇔ FINITE s ∧ CARD s = n

⊢ ∀f s. IMAGE f s = {f x | x ∈ s}

⊢ ∀f s t.
    INJ f s t ⇔
    (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ f x = f y ⇒ x = y

⊢ ∀x s. x INSERT s = {y | y = x ∨ y ∈ s}

⊢ ∀s t. s ∩ t = {x | x ∈ s ∧ x ∈ t}

⊢ ∀f s y. LINV f s y = THE (LINV_OPT f s y)

⊢ ∀f s y.
    LINV_OPT f s y =
    if y ∈ IMAGE f s then SOME (@x. x ∈ s ∧ f x = y) else NONE

⊢ ∀s. FINITE s ⇒
      (s ≠ ∅ ⇒ MAX_SET s ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ MAX_SET s) ∧
      (s = ∅ ⇒ MAX_SET s = 0)

⊢ MIN_SET = $LEAST

⊢ ∀set. POW set = {s | s ⊆ set}

⊢ ∀f s. PREIMAGE f s = {x | f x ∈ s}

⊢ ∀f s. Π f s = ITSET (λe acc. f e * acc) s 1

⊢ PROD_SET = Π I

⊢ ∀s t. s ⊂ t ⇔ s ⊆ t ∧ s ≠ t

⊢ ∀R s x y. REL_RESTRICT R s x y ⇔ x ∈ s ∧ y ∈ s ∧ R x y

⊢ ∀s. REST s = s DELETE CHOICE s

⊢ ∀f s y. RINV f s y = THE (LINV_OPT f s y)

⊢ ∀s. SING s ⇔ ∃x. s = {x}

⊢ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

⊢ ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0

⊢ SUM_SET = ∑ I

⊢ ∀f s t.
    SURJ f s t ⇔ (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∈ t ⇒ ∃y. y ∈ s ∧ f y = x

⊢ ∀s t. s ∪ t = {x | x ∈ s ∨ x ∈ t}

⊢ 𝕌(:α) = (λx. T)

⊢ (∀s. chooser s 0 = CHOICE s) ∧
  ∀s n. chooser s (SUC n) = chooser (REST s) n

⊢ ∀f s.
    closure_comm_assoc_fun f s ⇔
    (∀x y. x ∈ s ∧ y ∈ s ⇒ f x y ∈ s) ∧
    ∀x y z. x ∈ s ∧ y ∈ s ∧ z ∈ s ⇒ f x (f y z) = f y (f x z)

⊢ ∀n. count n = {m | m < n}

⊢ ∀s. countable s ⇔ ∃f. INJ f s 𝕌(:num)

⊢ ∀A B. A ⊔ B = {INL a | a ∈ A} ∪ {INR b | b ∈ B}

⊢ disjoint = pairwise (RC DISJOINT)

⊢ ∀s. enumerate s = @f. BIJ f 𝕌(:num) s

⊢ ∀R s.
    R equiv_on s ⇔
    (∀x. x ∈ s ⇒ R x x) ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ (R x y ⇔ R y x)) ∧
    ∀x y z. x ∈ s ∧ y ∈ s ∧ z ∈ s ∧ R x y ∧ R y z ⇒ R x z

⊢ ∀n. from n = {m | n ≤ m}

⊢ ∀m s x. is_measure_maximal m s x ⇔ x ∈ s ∧ ∀y. y ∈ s ⇒ m y ≤ m x

⊢ ∀n. num_to_pair n = (nfst n,nsnd n)

⊢ ∀m n. pair_to_num (m,n) = m ⊗ n

⊢ ∀P s. pairwise P s ⇔ ∀e1 e2. e1 ∈ s ∧ e2 ∈ s ⇒ P e1 e2

⊢ ∀v x. part v x = @s. x ∈ s ∧ s ∈ v

⊢ ∀R s. partition R s = {t | ∃x. x ∈ s ∧ t = equiv_class R s x}

⊢ ∀X Y. X partitions Y ⇔ ∃R. R equiv_on Y ∧ X = partition R Y

⊢ ∀v1 v2. v1 refines v2 ⇔ ∀s1. s1 ∈ v1 ⇒ ∃s2. s2 ∈ v2 ∧ s1 ⊆ s2

⊢ ∀f s x. schroeder_close f s x ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s

⊢ ∀x s. x ∈ s ⇔ x INSERT s = s

⊢ ∀x s. x ∈ s ⇒ x INSERT s = s

⊢ ∀s. FINITE s ⇒ ABS_DIFF (∑ f s) (∑ g s) ≤ ∑ (λx. ABS_DIFF (f x) (g x)) s

⊢ ∀P Q. BIGINTER {P; Q} = P ∩ Q

⊢ BIGINTER ∅ = 𝕌(:α)

⊢ (∀P f. BIGINTER {f x | P x} = {a | ∀x. P x ⇒ a ∈ f x}) ∧
  (∀P f. BIGINTER {f x y | P x y} = {a | ∀x y. P x y ⇒ a ∈ f x y}) ∧
  ∀P f. BIGINTER {f x y z | P x y z} = {a | ∀x y z. P x y z ⇒ a ∈ f x y z}

⊢ ∀f s. BIGINTER (IMAGE f s) = {y | ∀x. x ∈ s ⇒ y ∈ f x}

⊢ ∀P B. BIGINTER (P INSERT B) = P ∩ BIGINTER B

⊢ ∀P Q. BIGINTER {P; Q} = P ∩ Q

⊢ ∀P. BIGINTER {P} = P

⊢ ∀sp s t. t ∈ s ∧ t ⊆ sp ⇒ BIGINTER s ⊆ sp

⊢ ∀s1 s2. BIGINTER (s1 ∪ s2) = BIGINTER s1 ∩ BIGINTER s2

⊢ BIGINTER B x ⇔ ∀P. P ∈ B ⇒ x ∈ P

⊢ ∀f s t. BIGUNION (IMAGE f s) × t = BIGUNION (IMAGE (λn. f n × t) s)

⊢ BIGUNION ∅ = ∅

⊢ ∀P. (BIGUNION P = ∅ ⇔ P = ∅ ∨ P = {∅}) ∧
      (∅ = BIGUNION P ⇔ P = ∅ ∨ P = {∅})

⊢ (∀P f. BIGUNION {f x | P x} = {a | ∃x. P x ∧ a ∈ f x}) ∧
  (∀P f. BIGUNION {f x y | P x y} = {a | ∃x y. P x y ∧ a ∈ f x y}) ∧
  ∀P f. BIGUNION {f x y z | P x y z} = {a | ∃x y z. P x y z ∧ a ∈ f x y z}

⊢ ∀f s. BIGUNION (IMAGE f s) = {y | ∃x. x ∈ s ∧ y ∈ f x}

⊢ ∀f s t. BIGUNION (IMAGE f s) ⊆ t ⇔ ∀x. x ∈ s ⇒ f x ⊆ t

⊢ ∀f N.
    (∀n. N ≤ n ⇒ f n = ∅) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE f (count N))

⊢ ∀s P. BIGUNION (s INSERT P) = s ∪ BIGUNION P

⊢ ∀s t. BIGUNION {s; t} = s ∪ t

⊢ ∀x. BIGUNION {x} = x

⊢ ∀X P. BIGUNION P ⊆ X ⇔ ∀Y. Y ∈ P ⇒ Y ⊆ X

⊢ ∀s1 s2. BIGUNION (s1 ∪ s2) = BIGUNION s1 ∪ BIGUNION s2

⊢ ∀x sos. BIGUNION sos x ⇔ ∃s. x ∈ s ∧ s ∈ sos

⊢ R equiv_on s ⇒ BIGUNION (partition R s) = s

⊢ ∀f s t. BIJ f s t ⇔ f ∈ FUNSET s t ∧ ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ y = f x

⊢ ∀f g s t u. BIJ f s t ∧ BIJ g t u ⇒ BIJ (g ∘ f) s u

⊢ ∀f g s t. (∀x. x ∈ s ⇒ f x = g x) ⇒ (BIJ f s t ⇔ BIJ g s t)

⊢ ∀s t f. BIJ f s t ⇒ ∀e. e ∈ s ⇒ BIJ f (s DELETE e) (t DELETE f e)

⊢ ∀f s t x. BIJ f s t ∧ x ∈ s ⇒ f x ∈ t

⊢ ∀f. (∀s. BIJ f ∅ s ⇔ s = ∅) ∧ ∀s. BIJ f s ∅ ⇔ s = ∅

⊢ ∀f s t. BIJ f s t ∧ FINITE s ⇒ FINITE t

⊢ ∀f s t. BIJ f s t ⇒ (FINITE s ⇔ FINITE t)

⊢ ∀f s t. BIJ f 𝕌(:num) s ∧ FINITE t ∧ t ⊆ s ⇒ ∃N. ∀n. N ≤ n ⇒ f n ∉ t

⊢ ∀s. (λx. x) PERMUTES s

⊢ ∀f s t.
    BIJ f s t ⇔
    (∀x. x ∈ s ⇒ f x ∈ t) ∧
    ∃g. (∀x. x ∈ t ⇒ g x ∈ s) ∧ (∀x. x ∈ s ⇒ g (f x) = x) ∧
        ∀x. x ∈ t ⇒ f (g x) = x

⊢ ∀f s t. BIJ f s t ⇒ t = IMAGE f s

⊢ ∀f x y v. BIJ f x y ∧ v partitions x ⇒ IMAGE (IMAGE f) v partitions y

⊢ BIJ f 𝕌(:α) 𝕌(:β) ⇒ ∀x y. f x = f y ⇔ x = y

⊢ ∀s t. (∃f. INJ f s t) ∧ (∃g. SURJ g s t) ⇒ ∃h. BIJ h s t

⊢ ∀f e s t.
    BIJ f (e INSERT s) t ⇔
    e ∉ s ∧ f e ∈ t ∧ BIJ f s (t DELETE f e) ∨ e ∈ s ∧ BIJ f s t

⊢ ∀f e s t.
    e ∉ s ∧ BIJ f (e INSERT s) t ⇒
    ∃u. f e INSERT u = t ∧ f e ∉ u ∧ BIJ f s u

⊢ ∀f s t.
    BIJ f s t ⇒
    ∃g. BIJ g t s ∧ (∀x. x ∈ s ⇒ (g ∘ f) x = x) ∧ ∀x. x ∈ t ⇒ (f ∘ g) x = x

⊢ ∀f s t. BIJ f s t ⇒ ∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y

⊢ ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ ∃y. y ∈ s ∧ f y = x

⊢ ∀s. I PERMUTES s

⊢ ∀f s t. BIJ f s t ⇒ BIJ (LINV f s) t s

⊢ ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ f (LINV f s x) = x

⊢ ∀s. (∃f. BIJ f 𝕌(:num) s) ⇒ countable s

⊢ BIJ num_to_pair 𝕌(:num) (𝕌(:num) × 𝕌(:num))

⊢ BIJ pair_to_num (𝕌(:num) × 𝕌(:num)) 𝕌(:num)

⊢ BIJ SWAP (𝕌(:α) × 𝕌(:β)) (𝕌(:β) × 𝕌(:α))

⊢ ∀s t. (∃f. BIJ f s t) ⇔ ∃g. BIJ g t s

⊢ ∀s t. (∃f. BIJ f s t) ⇒ ∃g. BIJ g t s

⊢ ∀f s t.
    BIJ f s t ⇔ (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ f x = y

⊢ ∀s t u. (∃f. BIJ f s t) ∧ (∃g. BIJ g t u) ⇒ ∃h. BIJ h s u

⊢ ∀f s' s. f PERMUTES s' ∧ s' ⊆ s ∧ (∀x. x ∉ s' ⇒ f x = x) ⇒ f PERMUTES s

⊢ ∀s. FINITE s ⇒ CARD s = ∑ (λx. 1) s

⊢ ∀n s.
    FINITE s ∧ (∀e. e ∈ s ⇒ FINITE e ∧ CARD e = n) ∧
    (∀e1 e2. e1 ∈ s ∧ e2 ∈ s ∧ e1 ≠ e2 ⇒ DISJOINT e1 e2) ⇒
    CARD (BIGUNION s) = CARD s * n

⊢ CARD ∅ = 0 ∧
  ∀s. FINITE s ⇒
      ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

⊢ ∀n. CARD (count n) = n

⊢ ∀P Q. FINITE P ∧ FINITE Q ⇒ CARD (P × Q) = CARD P * CARD Q

⊢ ∀s. FINITE s ⇒
      ∀x. CARD (s DELETE x) = if x ∈ s then CARD s − 1 else CARD s

⊢ ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ CARD (s DIFF t) = CARD s − CARD (s ∩ t)

⊢ ∀t s. FINITE s ⇒ CARD (s DIFF t) = CARD s − CARD (s ∩ t)

⊢ CARD ∅ = 0

⊢ ∀s. FINITE s ⇒ (CARD s = 0 ⇔ s = ∅)

⊢ ∀s. FINITE s ⇒ CARD s = ∑ (K 1) s

⊢ ∀s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s

⊢ ∀f s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ FINITE s ⇒
    CARD (IMAGE f s) = CARD s

⊢ ∀f s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s

⊢ ∀s. FINITE s ⇒ CARD (IMAGE SUC s) = CARD s

⊢ ∀f s. (∀x y. f x = f y ⇔ x = y) ∧ FINITE s ⇒ CARD (IMAGE f s) = CARD s

⊢ ∀s. FINITE s ⇒
      ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

⊢ ∀s. FINITE s ⇒ ∀t. CARD (s ∩ t) ≤ CARD s

⊢ FINITE s ⇒ CARD s ≤ MAX_SET s + 1

⊢ ∀s. FINITE s ⇒ CARD (POW s) = 2 ** CARD s

⊢ ∀s t.
    FINITE s ∧ FINITE t ⇒ CARD {(x,y) | x ∈ s ∧ y ∈ t} = CARD s * CARD t

⊢ ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ CARD t < CARD s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ CARD (REST s) = CARD s − 1

⊢ ∀x. CARD {x} = 1

⊢ ∀x P. FINITE P ⇒ CARD ({x} × P) = CARD P

⊢ ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ CARD t ≤ CARD s

⊢ ∀s. FINITE s ⇒
      ∀t. FINITE t ⇒ CARD (s ∪ t) + CARD (s ∩ t) = CARD s + CARD t

⊢ ∀s t. FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒ CARD (s ∪ t) = CARD s + CARD t

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ CARD (s ∪ t) = CARD s + CARD t − CARD (s ∩ t)

⊢ FINITE s ∧ FINITE t ⇒ CARD (s ∪ t) ≤ CARD s + CARD t

⊢ FINITE s ∧ FINITE t ⇒ CARD (s ⊔ t) = CARD s + CARD t

⊢ ∀s. s ≠ ∅ ⇒ CHOICE s INSERT REST s = s

⊢ (∃x. x ∈ s) ∧ (∀x. x ∈ s ⇒ P x) ⇒ P (CHOICE s)

⊢ ∀s. CHOICE s ∉ REST s

⊢ ∀x. CHOICE {x} = x

⊢ ∀f s.
    (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
    ∀x b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)

⊢ ∀f e s b.
    (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
    ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b)

⊢ ∀s. COMPL s ∩ s = ∅ ∧ COMPL s ∪ s = 𝕌(:α)

⊢ ∀s. COMPL (COMPL s) = s

⊢ COMPL ∅ = 𝕌(:α)

⊢ x ∩ COMPL x = ∅ ∧ COMPL x ∩ x = ∅

⊢ ∀p q. p ∩ q ∪ COMPL p ∩ q = q

⊢ COMPL (s ∪ t) = COMPL s ∩ COMPL t

⊢ ∀x s. COMPL s x ⇔ x ∉ s

⊢ ∀x s. x ∈ x INSERT s

⊢ ∀s. countable s ⇔ ∃f. ∀x. x ∈ s ⇒ ∃n. f n = x

⊢ ∀s. countable s ⇔ FINITE s ∨ BIJ (enumerate s) 𝕌(:num) s

⊢ ∀n. countable (count n)

⊢ ∀c. countable c ⇔ c = ∅ ∨ ∃f. c = IMAGE f 𝕌(:num)

⊢ ∀n. countable (from n)

⊢ ∀f s. countable (IMAGE f s)

⊢ ∀s. countable s

⊢ ∀s t. s ⊆ t ∧ countable t ⇒ countable s

⊢ ∀n1 n2. count n1 = count n2 ⇔ n1 = n2

⊢ ∀n. count n DELETE n = count n

⊢ count n = ∅ ⇔ n = 0

⊢ ∀m n. m ≤ n ⇒ count m ⊆ count n

⊢ ∀n. 0 < n ⇔ count n ≠ ∅

⊢ count 1 = {0}

⊢ ∀n. count (SUC n) = n INSERT count n

⊢ count 0 = ∅

⊢ ∀m n. count n m ⇔ m < n

⊢ ∀f s t. s × BIGUNION (IMAGE f t) = BIGUNION (IMAGE (λn. s × f n) t)

⊢ ∀P. P × ∅ = ∅ ∧ ∅ × P = ∅

⊢ s × t = ∅ ⇔ s = ∅ ∨ t = ∅

⊢ ∀s1 s2. ∅ × s2 = ∅ ∧ (a INSERT s1) × s2 = IMAGE (λy. (a,y)) s2 ∪ s1 × s2

⊢ ∀P Q x. (x INSERT P) × Q = {x} × Q ∪ P × Q

⊢ ∀P Q x. P × (x INSERT Q) = P × {x} ∪ P × Q

⊢ ∀x y. {x} × {y} = {(x,y)}

⊢ ∀P Q P0 Q0. P0 × Q0 ⊆ P × Q ⇔ P0 = ∅ ∨ Q0 = ∅ ∨ P0 ⊆ P ∧ Q0 ⊆ Q

⊢ 𝕌(:α # β) = 𝕌(:α) × 𝕌(:β)

⊢ ∀P Q x. (P × Q) x ⇔ FST x ∈ P ∧ SND x ∈ Q

⊢ ∀s x. x ∈ s ⇔ ∃t. s = x INSERT t ∧ x ∉ t

⊢ ∀x y s. s DELETE x DELETE y = s DELETE y DELETE x

⊢ ∀x s. s DELETE x DELETE x = s DELETE x

⊢ ∀s x. x ∈ s ⇒ (s DELETE x = ∅ ⇔ s = {x})

⊢ ∀x y s.
    (x INSERT s) DELETE y =
    if x = y then s DELETE y else x INSERT s DELETE y

⊢ ∀s t x. (s DELETE x) ∩ t = s ∩ t DELETE x

⊢ ∀x s. x ∉ s ⇔ s DELETE x = s

⊢ ∀s x. x ∉ s ⇒ s DELETE x = s

⊢ ∀x s. s DELETE x ⊆ s

⊢ ∀s e s2. s DELETE e ⊆ s2 ⇔ s ⊆ e INSERT s2

⊢ ∀s x y. (s DELETE y) x ⇔ x ∈ s ∧ x ≠ y

⊢ ∀f P Q. DFUNSET P Q f ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x

⊢ ∀sp s.
    (∀t. t ∈ s ⇒ t ⊆ sp) ∧ s ≠ ∅ ⇒
    BIGINTER s = sp DIFF BIGUNION (IMAGE (λu. sp DIFF u) s)

⊢ ∀sp s. sp DIFF BIGINTER s = BIGUNION (IMAGE (λu. sp DIFF u) s)

⊢ ∀x y z. x DIFF y DIFF z = x DIFF z DIFF y

⊢ ∀s t. s DIFF t DIFF t = s DIFF t

⊢ ∀s t. t ⊆ s ⇒ s DIFF (s DIFF t) = t

⊢ ∀s. s DIFF ∅ = s

⊢ ∀s. s DIFF s = ∅

⊢ ∀s t x. s DIFF (x INSERT t) = s DELETE x DIFF t

⊢ ∀s t g. (s DIFF t) ∩ g = s ∩ g DIFF t

⊢ ∀s t. s DIFF t ∩ s = s DIFF t

⊢ ∀s t. s DIFF t = s ∩ COMPL t

⊢ ∀r s t. r ⊆ s ⇒ r DIFF s ∩ t = r DIFF t

⊢ ∀x y. x ∪ y DIFF x = y DIFF x ∧ x ∪ y DIFF y = x DIFF y

⊢ ∀s t. s DIFF t ⊆ s

⊢ ∀x y z. x DIFF (y ∪ z) = x DIFF y DIFF z

⊢ ∀s. s DIFF 𝕌(:α) = ∅

⊢ ∀s t x. (s DIFF t) x ⇔ x ∈ s ∧ x ∉ t

⊢ ∀s t. DISJOINT s t ⇔ ∀x. x ∈ s ⇒ x ∉ t

⊢ ∀s t. DISJOINT s t ⇔ ∀x. x ∈ t ⇒ x ∉ s

⊢ ∀X Y P.
    Y ∈ P ∧ DISJOINT Y X ⇒
    DISJOINT X (BIGINTER P) ∧ DISJOINT (BIGINTER P) X

⊢ (∀s t. DISJOINT (BIGUNION s) t ⇔ ∀s'. s' ∈ s ⇒ DISJOINT s' t) ∧
  ∀s t. DISJOINT t (BIGUNION s) ⇔ ∀s'. s' ∈ s ⇒ DISJOINT t s'

⊢ ∀f. (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
      ∀n. DISJOINT (f n) (BIGUNION (IMAGE f (count n)))

⊢ ∀n. DISJOINT (count n) (from n)

⊢ ∀s t x. DISJOINT (s DELETE x) t ⇔ DISJOINT (t DELETE x) s

⊢ ∀s t. DISJOINT t (s DIFF t) ∧ DISJOINT (s DIFF t) t

⊢ ∀f g m n.
    (∀n. f n ⊆ f (SUC n)) ∧ (∀n. g n = f (SUC n) DIFF f n) ∧ m ≠ n ⇒
    DISJOINT (g m) (g n)

⊢ ∀s. DISJOINT ∅ s ∧ DISJOINT s ∅

⊢ ∀s. s = ∅ ⇔ DISJOINT s s

⊢ ∀s. DISJOINT s s ⇔ s = ∅

⊢ ∀n. DISJOINT (from n) (count n)

⊢ (∀x y. f x = f y ⇔ x = y) ⇒
  (DISJOINT (IMAGE f s1) (IMAGE f s2) ⇔ DISJOINT s1 s2)

⊢ ∀x s t. DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t

⊢ ∀x s t. DISJOINT t (x INSERT s) ⇔ DISJOINT t s ∧ x ∉ t

⊢ ∀x. DISJOINT {x} ∅

⊢ ∀s t u. DISJOINT s t ∧ u ⊆ t ⇒ DISJOINT s u

⊢ ∀s t u. DISJOINT s t ∧ u ⊆ s ⇒ DISJOINT u t

⊢ ∀s t. DISJOINT s t ⇔ DISJOINT t s

⊢ ∀s t u. DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u

⊢ ∀s t u. DISJOINT u (s ∪ t) ⇔ DISJOINT u s ∧ DISJOINT u t

⊢ ∀s t u.
    (DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u) ∧
    (DISJOINT u (s ∪ t) ⇔ DISJOINT s u ∧ DISJOINT t u)

⊢ ∀x s. x ∉ s DELETE x

⊢ ∀x. ∅ DELETE x = ∅

⊢ ∀s. ∅ DIFF s = ∅

⊢ ∀s. FUNSET ∅ s = 𝕌(:α -> β)

⊢ ∀s. ∅ ∈ POW s

⊢ R equiv_on s ⇒ ∅ ∉ partition R s

⊢ ∅ ≠ 𝕌(:α)

⊢ ∀s. ∅ ⊆ s

⊢ ∀s t. s ∪ t = ∅ ⇔ s = ∅ ∧ t = ∅

⊢ ∅ x ⇔ F

⊢ ∀s. (∃f. BIJ f 𝕌(:num) s) ⇔ BIJ (enumerate s) 𝕌(:num) s

⊢ ∀x y. {x} = {y} ⇔ x = y

⊢ ∀s t. s = t ⇒ s ⊆ t ∧ t ⊆ s

⊢ (∀x. x ∈ s) ⇔ s = 𝕌(:α)

⊢ ∀P f s. (∃y. y ∈ IMAGE f s ∧ P y) ⇔ ∃x. x ∈ s ∧ P (f x)

⊢ ∀P a s. (∃x. x ∈ a INSERT s ∧ P x) ⇔ P a ∨ ∃x. x ∈ s ∧ P x

⊢ ∀n s. FUNPOW REST n s ⊆ s

⊢ ∀n s. INFINITE s ⇒ FUNPOW REST n s ≠ ∅

⊢ ∀s t. s = t ⇔ ∀x. x ∈ s ⇔ x ∈ t

⊢ ∀s. EXTENSIONAL s = {f | ∀x. x ∉ s ⇒ f x = ARB}

⊢ EXTENSIONAL ∅ = {(λx. ARB)}

⊢ ∀s f g.
    f ∈ EXTENSIONAL s ∧ g ∈ EXTENSIONAL s ∧ (∀x. x ∈ s ⇒ f x = g x) ⇒ f = g

⊢ ∀f. EXTENSIONAL 𝕌(:α) f

⊢ ∀f. (∀x. FINITE {y | x = f y}) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s

⊢ (∃s. s ∈ P ∧ FINITE s) ⇒ FINITE (BIGINTER P)

⊢ ∀P. FINITE P ∧ (∀s. s ∈ P ⇒ FINITE s) ⇒ FINITE (BIGUNION P)

⊢ ∀P. FINITE (BIGUNION P) ⇔ FINITE P ∧ ∀s. s ∈ P ⇒ FINITE s

⊢ ∀f s t. FINITE s ∧ BIJ f s t ⇒ FINITE t ∧ CARD s = CARD t

⊢ ∀f s t. FINITE s ∧ BIJ f s t ⇒ CARD s = CARD t

⊢ ∀S. FINITE S ⇒ ∀t f. BIJ f S t ∧ FINITE t ⇒ CARD S = CARD t

⊢ ∀s. FINITE s ⇒ ∃f b. BIJ f (count b) s

⊢ ∀s. FINITE s ⇔ ∃c n. BIJ c (count n) s

⊢ ∀s f. (∀x y. f x = f y ⇔ x = y) ∧ FINITE s ⇒ CARD (IMAGE f s) = CARD s

⊢ ∀P. (∀x. (∀y. y ⊂ x ⇒ P y) ⇒ FINITE x ⇒ P x) ⇒ ∀x. FINITE x ⇒ P x

⊢ ∀n. FINITE (count n)

⊢ ∀P Q. FINITE P ∧ FINITE Q ⇒ FINITE (P × Q)

⊢ ∀P Q. FINITE (P × Q) ⇔ P = ∅ ∨ Q = ∅ ∨ FINITE P ∧ FINITE Q

⊢ ∀x s. FINITE (s DELETE x) ⇔ FINITE s

⊢ ∀s. FINITE s ⇒ ∀t. FINITE (s DIFF t)

⊢ ∀P Q. FINITE (P DIFF Q) ∧ FINITE Q ⇒ FINITE P

⊢ FINITE ∅

⊢ ∀s. FINITE s ⇔ s HAS_SIZE CARD s

⊢ (∀x y. x ∈ s ∧ y ∈ s ⇒ (f x = f y ⇔ x = y)) ⇒
  (FINITE (IMAGE f s) ⇔ FINITE s)

⊢ ∀f s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    (FINITE (IMAGE f s) ⇔ FINITE s)

⊢ ∀P. P ∅ ∧ (∀s. FINITE s ∧ P s ⇒ ∀e. e ∉ s ⇒ P (e INSERT s)) ⇒
      ∀s. FINITE s ⇒ P s

⊢ ∀P. P ∅ ∧ (∀x s. P s ∧ x ∉ s ∧ FINITE s ⇒ P (x INSERT s)) ⇒
      ∀s. FINITE s ⇒ P s

⊢ ∀f s t. INJ f s t ∧ FINITE t ⇒ FINITE s

⊢ ∀x s. FINITE (x INSERT s) ⇔ FINITE s

⊢ ∀s1 s2. FINITE s1 ∨ FINITE s2 ⇒ FINITE (s1 ∩ s2)

⊢ ∀s. FINITE s ⇒
      ∃f. (∀n m. n < CARD s ∧ m < CARD s ⇒ f n = f m ⇒ n = m) ∧
          s = {f n | n < CARD s}

⊢ ∀f P.
    P ∅ ∧ (∀a s. a ∉ s ∧ (∀b. b ∈ s ⇒ f a ≤ f b) ∧ P s ⇒ P (a INSERT s)) ⇒
    ∀s. FINITE s ⇒ P s

⊢ ∀s. FINITE s ⇒ FINITE (POW s)

⊢ FINITE (POW s) ⇔ FINITE s

⊢ (∀x y. f x = f y ⇔ x = y) ∧ FINITE s ⇒ FINITE (PREIMAGE f s)

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE {(x,y) | x ∈ s ∧ y ∈ t}

⊢ ∀f s t.
    FINITE s ∧ (∀x. x ∈ s ⇒ FINITE (t x)) ⇒
    FINITE {f x y | x ∈ s ∧ y ∈ t x}

⊢ ∀s. INFINITE s ⇔ ∀t. FINITE t ⇒ t ⊆ s ⇒ t ⊂ s

⊢ INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ s ⊂ 𝕌(:α)

⊢ ∀s. FINITE s ⇒ FINITE (REST s)

⊢ ∀s. FINITE (REST s) ⇔ FINITE s

⊢ FINITE ∅ ∧ ∀s. FINITE s ⇒ ∀x. FINITE (x INSERT s)

⊢ ∀x. FINITE {x}

⊢ FINITE s ∧ SURJ f s t ⇒ FINITE t

⊢ FINITE s ∧ SURJ f s t ∧ CARD t = CARD s ⇒ BIJ f s t

⊢ ∀R s. FINITE s ∧ StrongOrder (REL_RESTRICT R s) ⇒ WF (REL_RESTRICT R s)

⊢ ∀s t. FINITE (s ∪ t) ⇔ FINITE s ∧ FINITE t

⊢ ∀s. FINITE s ⇔ ∃f b. ∀e. e ∈ s ⇔ ∃n. n < b ∧ e = f n

⊢ ∀s. FINITE s ⇒ (WF (REL_RESTRICT R s) ⇔ irreflexive (REL_RESTRICT R s)⁺)

⊢ ∀m s. FINITE s ∧ s ≠ ∅ ⇒ ∃x. is_measure_maximal m s x

⊢ ∀R s.
    FINITE s ⇒ FINITE (partition R s) ∧ ∀t. t ∈ partition R s ⇒ FINITE t

⊢ ∀x. FINITE x ⇒ FINITE {v | v partitions x}

⊢ ∀P s. (∀x. x ∈ BIGUNION s ⇒ P x) ⇔ ∀t x. t ∈ s ∧ x ∈ t ⇒ P x

⊢ ∀P f s. (∀y. y ∈ IMAGE f s ⇒ P y) ⇔ ∀x. x ∈ s ⇒ P (f x)

⊢ ∀P a s. (∀x. x ∈ a INSERT s ⇒ P x) ⇔ P a ∧ ∀x. x ∈ s ⇒ P x

⊢ ∀P s t. (∀x. x ∈ s ∪ t ⇒ P x) ⇔ (∀x. x ∈ s ⇒ P x) ∧ ∀x. x ∈ t ⇒ P x

⊢ from 0 = 𝕌(:num)

⊢ ∀n. from n ≠ ∅

⊢ ∀m n. from n m ⇔ n ≤ m

⊢ INJ f 𝕌(:α) 𝕌(:α) ⇒ INJ (FUNPOW f n) 𝕌(:α) 𝕌(:α)

⊢ INJ f 𝕌(:α) 𝕌(:α) ⇒ (FUNPOW f n t = FUNPOW f n t' ⇔ t = t')

⊢ n ≤ n' ∧ INJ f 𝕌(:α) 𝕌(:α) ⇒
  (FUNPOW f n X = FUNPOW f n' X' ⇔ X = FUNPOW f (n' − n) X')

⊢ ∀x y. FUNSET x y = DFUNSET x (K y)

⊢ ∀s f. f ∈ FUNSET s ∅ ⇔ s = ∅

⊢ ∀a b c. FUNSET a (b ∩ c) = FUNSET a b ∩ FUNSET a c

⊢ ∀s t f x. f ∈ FUNSET s t ∧ x ∈ s ⇒ f x ∈ t

⊢ ∀f P Q. FUNSET P Q f ⇔ ∀x. x ∈ P ⇒ f x ∈ Q

⊢ ∀f v. GSPEC f v ⇔ ∃x. (v,T) = f x

⊢ ∀P Q. {x | P x ∧ Q x} = {x | P x} ∩ {x | Q x}

⊢ {x | x = y} = {y}

⊢ {x | y = x} = {y}

⊢ {x | P x} = P

⊢ {x | F} = ∅

⊢ ∀f. (∀x. ¬SND (f x)) ⇒ GSPEC f = ∅

⊢ {x | x ∈ y} = y

⊢ GSPEC f = IMAGE (FST ∘ f) (SND ∘ f)

⊢ ∀P Q. {x | P x ∨ Q x} = {x | P x} ∪ {x | Q x}

⊢ {(x,y) | P x y} = UNCURRY P

⊢ {x | T} = 𝕌(:α)

⊢ ∀s. s HAS_SIZE 0 ⇔ s = ∅

⊢ ∀s n. s HAS_SIZE n ⇒ CARD s = n

⊢ ∀f s n.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ s HAS_SIZE n ⇒
    IMAGE f s HAS_SIZE n

⊢ ∀s n.
    s HAS_SIZE n ⇒
    ∃f. (∀m. m < n ⇒ f m ∈ s) ∧ ∀x. x ∈ s ⇒ ∃!m. m < n ∧ f m = x

⊢ ∀s m t n.
    s HAS_SIZE m ∧ t HAS_SIZE n ⇒ {(x,y) | x ∈ s ∧ y ∈ t} HAS_SIZE m * n

⊢ ∀s m t n.
    s HAS_SIZE m ∧ (∀x. x ∈ s ⇒ t x HAS_SIZE n) ⇒
    {(x,y) | x ∈ s ∧ y ∈ t x} HAS_SIZE m * n

⊢ ∀s n. s HAS_SIZE SUC n ⇔ s ≠ ∅ ∧ ∀a. a ∈ s ⇒ s DELETE a HAS_SIZE n

⊢ ∀s t m n.
    s HAS_SIZE m ∧ t HAS_SIZE n ∧ DISJOINT s t ⇒ s ∪ t HAS_SIZE m + n

⊢ (∀x y. f x = f y ⇔ x = y) ⇒ (IMAGE f s1 = IMAGE f s2 ⇔ s1 = s2)

⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇒ ∀s. INFINITE s ⇒ INFINITE (IMAGE f s)

⊢ ∀f M. IMAGE f (BIGUNION M) = BIGUNION (IMAGE (IMAGE f) M)

⊢ (∀f. IMAGE f ∅ = ∅) ∧ ∀f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s

⊢ ∀f g s. IMAGE (f ∘ g) s = IMAGE f (IMAGE g s)

⊢ ∀f s f' s'. s = s' ∧ (∀x. x ∈ s' ⇒ f x = f' x) ⇒ IMAGE f s = IMAGE f' s'

⊢ ∀s c. IMAGE (λx. c) s = if s = ∅ then ∅ else {c}

⊢ ∀f x s. x ∉ s ⇒ IMAGE f (s DELETE x) = IMAGE f s

⊢ ∀f. IMAGE f ∅ = ∅

⊢ ∀s f. (IMAGE f s = ∅ ⇔ s = ∅) ∧ (∅ = IMAGE f s ⇔ s = ∅)

⊢ IMAGE f s = {z} ⇔ s ≠ ∅ ∧ ∀x. x ∈ s ⇒ f x = z

⊢ ∀s. FINITE s ⇒ ∀f. FINITE (IMAGE f s)

⊢ ∀s t. t ≠ ∅ ⇒ IMAGE FST (s × t) = s

⊢ IMAGE I s = s

⊢ ∀s. IMAGE (λx. x) s = s

⊢ IMAGE I = I

⊢ ∀f g s. IMAGE f (IMAGE g s) = IMAGE (f ∘ g) s

⊢ ∀R f s t.
    INJ f s t ⇒
    IMAGE (IMAGE f) (partition R s) =
    partition (inv_image R (LINV f s)) (IMAGE f s)

⊢ ∀x s. x ∈ s ⇒ ∀f. f x ∈ IMAGE f s

⊢ ∀f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s

⊢ ∀f s t. IMAGE f (s ∩ t) ⊆ IMAGE f s ∩ IMAGE f t

⊢ ∀f s. IMAGE f (PREIMAGE f s) ⊆ s

⊢ ∀f s t. s ⊆ t ⇒ IMAGE (RESTRICTION t f) s = IMAGE f s

⊢ ∀f x. IMAGE f {x} = {f x}

⊢ ∀s t. s ≠ ∅ ⇒ IMAGE SND (s × t) = t

⊢ ∀s t. s ⊆ t ⇒ ∀f. IMAGE f s ⊆ IMAGE f t

⊢ ∀f s u t. s ⊆ u ∧ IMAGE f u ⊆ t ⇒ IMAGE f s ⊆ t

⊢ ∀f s t. SURJ f s t ⇔ IMAGE f s = t

⊢ ∀f s t. IMAGE f (s ∪ t) = IMAGE f s ∪ IMAGE f t

⊢ ∀y s f. IMAGE f s y ⇔ ∃x. y = f x ∧ x ∈ s

⊢ ∀f g s. IMAGE (f ∘ g) s = IMAGE f (IMAGE g s)

⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ s DIFF t ≠ ∅

⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ INFINITE (s DIFF t)

⊢ ∀s. INFINITE s ⇒ INJ (λn. CHOICE (FUNPOW REST n s)) 𝕌(:num) s

⊢ ∀P. INFINITE P ⇒ ∃x. x ∈ P

⊢ ∀f s t. INJ f s t ∧ INFINITE s ⇒ INFINITE t

⊢ ∀s. INFINITE s ⇔ ∃f. INJ f s s ∧ ¬SURJ f s s

⊢ INFINITE 𝕌(:num)

⊢ FINITE 𝕌(:α # β) ⇔ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β)

⊢ ∀s. INFINITE s ⇒ ∀t. s ⊆ t ⇒ INFINITE t

⊢ INFINITE 𝕌(:α) ⇔ ∃f. (∀x y. f x = f y ⇒ x = y) ∧ ∃y. ∀x. f x ≠ y

⊢ ∀f. (∀x y. f x = f y ⇔ x = y) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s

⊢ s0 ⊆ s ∧ INJ f s t ⇒ BIJ f s0 (IMAGE f s0)

⊢ ∀f s t. INJ f s t ∧ FINITE t ⇒ CARD s ≤ CARD t

⊢ ∀s. FINITE s ⇒ INJ f s t ⇒ CARD (IMAGE f s) = CARD s

⊢ INJ f s t ⇒ FINITE s ⇒ CARD (IMAGE f s) = CARD s

⊢ ∀f g s t u. INJ f s t ∧ INJ g t u ⇒ INJ (g ∘ f) s u

⊢ ∀f g s t. (∀x. x ∈ s ⇒ f x = g x) ⇒ (INJ f s t ⇔ INJ g s t)

⊢ ∀f s t. INJ f s t ⇒ ∀e. e ∈ s ⇒ INJ f (s DELETE e) (t DELETE f e)

⊢ ∀f s t x. INJ f s t ∧ x ∈ s ⇒ f x ∈ t

⊢ ∀f. (∀s. INJ f ∅ s) ∧ ∀s. INJ f s ∅ ⇔ s = ∅

⊢ ∀f s x y. INJ f s s ∧ x ∈ s ∧ y ∈ s ⇒ (f x = f y ⇔ x = y)

⊢ ∀b s t x y.
    INJ b s t ∧ x ∉ s ∧ y ∉ t ⇒ INJ b⦇x ↦ y⦈ (x INSERT s) (y INSERT t)

⊢ ∀s. INJ I s 𝕌(:α)

⊢ ∀s. INJ (λx. x) s s

⊢ INJ f s t ⇔
  (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ (f x = f y ⇔ x = y)

⊢ ∀f s t. INJ f s t ⇒ INJ f s (IMAGE f s)

⊢ ∀s f. (∃t. INJ f s t) ⇒ BIJ f s (IMAGE f s)

⊢ ∀P f.
    INJ f P 𝕌(:β) ⇒
    ∀s t. s ⊆ P ∧ t ⊆ P ⇒ (DISJOINT s t ⇔ DISJOINT (IMAGE f s) (IMAGE f t))

⊢ ∀P f.
    INJ f P 𝕌(:β) ⇒ ∀s t. s ⊆ P ∧ t ⊆ P ⇒ (IMAGE f s = IMAGE f t ⇔ s = t)

⊢ ∀P f.
    INJ f P 𝕌(:β) ⇒
    ∀s t. s ⊆ P ∧ t ⊆ P ⇒ IMAGE f (s ∩ t) = IMAGE f s ∩ IMAGE f t

⊢ ∀f s t. INJ f s t ⇒ IMAGE f s ⊆ t

⊢ ∀f s t x.
    INJ f s t ∧ x ∈ s ⇒
    IMAGE f (equiv_class R s x) =
    equiv_class (inv_image R (LINV f s)) (IMAGE f s) (f x)

⊢ ∀f. INJ f 𝕌(:α) 𝕌(:β) ⇒ ∀x y. f x = f y ⇔ x = y

⊢ (∀x. x ∈ s ⇒ INL x ∈ t) ⇒ INJ INL s t

⊢ (∀x. x ∈ s ⇒ INR x ∈ t) ⇒ INJ INR s t

⊢ ∀f x s t.
    INJ f (x INSERT s) t ⇔
    INJ f s t ∧ f x ∈ t ∧ ∀y. y ∈ s ∧ f x = f y ⇒ x = y

⊢ ∀s f. INJ I (IMAGE f s) 𝕌(:β)

⊢ INJ f s t ⇒ ∀x y. LINV_OPT f s y = SOME x ⇔ y = f x ∧ x ∈ s ∧ y ∈ t

⊢ INJ (LINV_OPT f s) (IMAGE f s) (IMAGE SOME s)

⊢ ∀f s t s0 t0. INJ f s t ∧ s0 ⊆ s ∧ t ⊆ t0 ⇒ INJ f s0 t0

⊢ ∀f s. INJ f 𝕌(:α) 𝕌(:β) ⇒ INJ f s 𝕌(:β)

⊢ ∀x y s. x INSERT y INSERT s = y INSERT x INSERT s

⊢ ∀x s. x ∈ s ⇒ x INSERT s DELETE x = s

⊢ ∀s t x.
    (x INSERT s) DIFF t = if x ∈ t then s DIFF t else x INSERT s DIFF t

⊢ ∀s x y. x INSERT s = {y} ⇔ x = y ∧ s ⊆ {y}

⊢ ∀x s. x INSERT x INSERT s = x INSERT s

⊢ ∀x s t. (x INSERT s) ∩ t = if x ∈ t then x INSERT s ∩ t else s ∩ t

⊢ ∀s x. x INSERT s = {x} ∪ s

⊢ ∀x s t. x INSERT s ⊆ t ⇔ x ∈ t ∧ s ⊆ t

⊢ ∀x s t. (x INSERT s) ∪ t = if x ∈ t then s ∪ t else x INSERT s ∪ t

⊢ ∀x s t. (x INSERT s) ∪ t = x INSERT s ∪ t

⊢ ∀x. x INSERT 𝕌(:α) = 𝕌(:α)

⊢ ∀x y s. (y INSERT s) x ⇔ x = y ∨ x ∈ s

⊢ ∀s t u. s ∩ (t ∩ u) = s ∩ t ∩ u

⊢ (∀s t. BIGUNION s ∩ t = BIGUNION {x ∩ t | x ∈ s}) ∧
  ∀s t. t ∩ BIGUNION s = BIGUNION {t ∩ x | x ∈ s}

⊢ ∀s t. s ∩ t = t ∩ s

⊢ ∀A B C D. A × B ∩ C × D = (A ∩ C) × (B ∩ D)

⊢ (∀s. ∅ ∩ s = ∅) ∧ ∀s. s ∩ ∅ = ∅

⊢ ∀s. FINITE s ⇒ ∀t. FINITE (s ∩ t)

⊢ ∀s. s ∩ s = s

⊢ ∀s t u. s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

⊢ ∀s x. x ∈ s ⇒ s ∩ {x} = {x}

⊢ (∀s t. s ∩ t ⊆ s) ∧ ∀s t. t ∩ s ⊆ s

⊢ (A ∩ B = A ⇔ A ⊆ B) ∧ (A ∩ B = B ⇔ B ⊆ A)

⊢ (A ∪ B) ∩ A = A ∧ (B ∪ A) ∩ A = A ∧ A ∩ (A ∪ B) = A ∧ A ∩ (B ∪ A) = A

⊢ ∀s t. s ∩ t = COMPL (COMPL s ∪ COMPL t)

⊢ (∀s. 𝕌(:α) ∩ s = s) ∧ ∀s. s ∩ 𝕌(:α) = s

⊢ ∀s t x. (s ∩ t) x ⇔ x ∈ s ∧ x ∈ t

⊢ ∀x P. x ∈ (λx. P x) ⇔ P x

⊢ ∀x P. x ∈ P ⇔ P x

⊢ x ∈ BIGINTER B ⇔ ∀P. P ∈ B ⇒ x ∈ P

⊢ ∀x f s. x ∈ BIGINTER (IMAGE f s) ⇔ ∀y. y ∈ s ⇒ x ∈ f y

⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s. x ∈ s ∧ s ∈ sos

⊢ ∀f s y. y ∈ BIGUNION (IMAGE f s) ⇔ ∃x. x ∈ s ∧ y ∈ f x

⊢ ∀x s. x ∈ COMPL s ⇔ x ∉ s

⊢ ∀m n. m ∈ count n ⇔ m < n

⊢ ∀P Q x. x ∈ P × Q ⇔ FST x ∈ P ∧ SND x ∈ Q

⊢ ∀s x y. x ∈ s DELETE y ⇔ x ∈ s ∧ x ≠ y

⊢ ∀s x x'. (x ∈ s ⇔ x' ∈ s) ⇔ (x ∈ s DELETE x' ⇔ x' ∈ s DELETE x)

⊢ ∀f P Q. f ∈ DFUNSET P Q ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x

⊢ ∀s t x. x ∈ s DIFF t ⇔ x ∈ s ∧ x ∉ t

⊢ ∀s t. DISJOINT s t ⇔ ¬∃x. x ∈ s ∧ x ∈ t

⊢ ∀s. s = 𝕌(:α) ⇒ ∀v. v ∈ s

⊢ ∀m n. m ∈ from n ⇔ n ≤ m

⊢ ∀f P Q. f ∈ FUNSET P Q ⇔ ∀x. x ∈ P ⇒ f x ∈ Q

⊢ ∀y x P. P y ∧ x = f y ⇒ x ∈ {f x | P x}

⊢ y ∈ {x | P x} ⇔ P y

⊢ ∀y s f. y ∈ IMAGE f s ⇔ ∃x. y = f x ∧ x ∈ s

⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ ∃x. x ∈ s ∧ x ∉ t

⊢ ∀x y s. x ∈ y INSERT s ⇔ x = y ∨ x ∈ s

⊢ ∀x y P. x ∈ y INSERT P ⇔ x = y ∨ x ≠ y ∧ x ∈ P

⊢ ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t

⊢ ∀set e. e ∈ POW set ⇔ e ⊆ set

⊢ ∀f s x. x ∈ PREIMAGE f s ⇔ f x ∈ s

⊢ ∀x s. x ∈ REST s ⇔ x ∈ s ∧ x ≠ CHOICE s

⊢ ∀x y. x ∈ {y} ⇔ x = y

⊢ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

⊢ ∀x. x ∈ 𝕌(:α)

⊢ (INL a ∈ A ⊔ B ⇔ a ∈ A) ∧ (INR b ∈ A ⊔ B ⇔ b ∈ B)

⊢ ∀f g. f = g ⇒ ITSET f = ITSET g

⊢ ∀f b. ITSET f ∅ b = b

⊢ ∀P. (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
      ∀v v1. P v v1

⊢ ∀s. FINITE s ⇒
      ∀f x b.
        ITSET f (x INSERT s) b =
        ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b)

⊢ ∀s f b.
    FINITE s ∧ s ≠ ∅ ⇒ ITSET f s b = ITSET f (REST s) (f (CHOICE s) b)

⊢ ∀f. (∀x y z. f x (f y z) = f y (f x z)) ⇒
      ∀s x b. FINITE s ∧ x ∉ s ⇒ ITSET f (x INSERT s) b = f x (ITSET f s b)

⊢ ∀f x a. ITSET f {x} a = f x a

⊢ ∀s f b.
    FINITE s ⇒
    ITSET f s b = if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b)

⊢ ∀s f b.
    ITSET f s b =
    if FINITE s then if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b)
    else ARB

⊢ ∀x y. K x ⊆ y ⇔ ¬x ∨ 𝕌(:α) ⊆ y

⊢ ∀R. (∀x. FINITE {y | R x y}) ⇒
      ∀x. INFINITE {y | R꙳ x y} ⇒ ∃f. f 0 = x ∧ ∀n. R (f n) (f (SUC n))

⊢ ∀R. (∀x. FINITE {y | R x y}) ∧ WF Rᵀ ⇒ ∀x. FINITE {y | R꙳ x y}

⊢ ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ CARD t < CARD s ⇒ 0 < CARD (s DIFF t)

⊢ ∀f s t. INJ f s t ⇒ ∀x. x ∈ s ⇒ LINV f s (f x) = x

⊢ LINV_OPT f s y = SOME x ⇒ x ∈ s ∧ f x = y

⊢ ∀P Q.
    FINITE P ∧ (P = ∅ ⇒ Q 0) ∧ (∀x. (∀y. y ∈ P ⇒ y ≤ x) ∧ x ∈ P ⇒ Q x) ⇒
    Q (MAX_SET P)

⊢ MAX_SET ∅ = 0

⊢ ∀s. FINITE s ⇒ (MAX_SET s = 0 ⇔ s = ∅ ∨ s = {0})

⊢ ∀A B. FINITE A ∧ FINITE B ⇒ MAX_SET (A ∩ B) ≤ MIN (MAX_SET A) (MAX_SET B)

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ MAX_SET s ∈ s

⊢ ∀s n. FINITE s ∧ MAX_SET s < n ⇒ ∀x. x ∈ s ⇒ x < n

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s

⊢ MAX_SET ∅ = 0 ∧ MAX_SET {e} = e

⊢ ∀e. MAX_SET {e} = e

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀x. x ∈ s ∧ (∀y. y ∈ s ⇒ y ≤ x) ⇒ x = MAX_SET s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀x. x ∈ s ⇒ (MAX_SET s = x ⇔ ∀y. y ∈ s ⇒ y ≤ x)

⊢ MAX_SET ∅ = 0 ∧ ∀e s. FINITE s ⇒ MAX_SET (e INSERT s) = MAX e (MAX_SET s)

⊢ ∀A B. FINITE A ∧ FINITE B ⇒ MAX_SET (A ∪ B) = MAX (MAX_SET A) (MAX_SET B)

⊢ ∀s. (∃x. x ∈ s) ⇔ s ≠ ∅

⊢ ∀P Q. P ≠ ∅ ∧ (∀x. (∀y. y ∈ P ⇒ x ≤ y) ∧ x ∈ P ⇒ Q x) ⇒ Q (MIN_SET P)

⊢ ∀s. s ≠ ∅ ⇒ (MIN_SET s = 0 ⇔ 0 ∈ s)

⊢ ∀s. s ≠ ∅ ⇒ MIN_SET s ∈ s

⊢ ∀s. s ≠ ∅ ⇒ MIN_SET s ∈ s ∧ ∀x. x ∈ s ⇒ MIN_SET s ≤ x

⊢ ∀s. s ≠ ∅ ∧ FINITE s ⇒ MIN_SET s ≤ MAX_SET s

⊢ ∀s. s ≠ ∅ ⇒ ∀x. x ∈ s ⇒ MIN_SET s ≤ x

⊢ ∀e. MIN_SET {e} = e

⊢ ∀s. s ≠ ∅ ⇒ ∀x. x ∈ s ∧ (∀y. y ∈ s ⇒ x ≤ y) ⇒ x = MIN_SET s

⊢ ∀s. s ≠ ∅ ⇒ ∀x. x ∈ s ⇒ (MIN_SET s = x ⇔ ∀y. y ∈ s ⇒ x ≤ y)

⊢ (∀e. MIN_SET {e} = e) ∧
  ∀s e1 e2.
    MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))

⊢ (∀e. MIN_SET {e} = e) ∧
  ∀e s. s ≠ ∅ ⇒ MIN_SET (e INSERT s) = MIN e (MIN_SET s)

⊢ ∀A B.
    FINITE A ∧ FINITE B ∧ A ≠ ∅ ∧ B ≠ ∅ ⇒
    MIN_SET (A ∪ B) = MIN (MIN_SET A) (MIN_SET B)

⊢ ∀x s. ∅ ≠ x INSERT s

⊢ ∀x. ∅ ≠ {x}

⊢ ∀s t. s ≠ t ⇔ ∃x. x ∈ t ⇔ x ∉ s

⊢ ∀x s. x INSERT s ≠ ∅

⊢ ∀x. x ∉ ∅

⊢ INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ ∃x. x ∉ s

⊢ ∀s. ¬(s ⊂ ∅)

⊢ ∀x. {x} ≠ ∅

⊢ ∀s. ¬(𝕌(:α) ⊂ s)

⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) 𝕌(:num)

⊢ ∀f N.
    BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    ∃k. IMAGE f (count N) ⊆ count k × count k

⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num))

⊢ ∃f. BIJ f (𝕌(:num) × (𝕌(:num) DIFF {0})) 𝕌(:num)

⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) (𝕌(:num) DIFF {0})

⊢ ∃f. BIJ f ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0})) 𝕌(:num)

⊢ ∃f. BIJ f 𝕌(:num) ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0}))

⊢ ∃f. BIJ f (𝕌(:num) DIFF {0}) (𝕌(:num) × 𝕌(:num))

⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × (𝕌(:num) DIFF {0}))

⊢ ∀f k.
    BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    ∃N. count k × count k ⊆ IMAGE f (count N)

⊢ ∀s. (∃n. n ∈ s) ⇔ ∃n. n ∈ s ∧ ∀m. m ∈ s ⇒ n ≤ m

⊢ ∀s a. s ≠ ∅ ∧ (∀k. k ∈ s ⇒ k = a) ⇒ s = {a}

⊢ (a,b) ∈ {(y,x) | P y} ⇔ P a ∧ b = x

⊢ (a,b) ∈ {(x,y) | P y} ⇔ P b ∧ a = x

⊢ (x,y) ∈ {(x,y) | P x y} ⇔ P x y

⊢ (a,b) ∈ {(x,x) | P x} ⇔ P a ∧ a = b

⊢ ∀f s t. FINITE t ∧ CARD t < CARD s ⇒ ¬INJ f s t

⊢ ∀s. FINITE s ⇒ ∀f k. (∀x. x ∈ s ⇒ f x = k) ⇒ Π f s = k ** CARD s

⊢ ∀s. POW s ≠ ∅

⊢ POW ∅ = {∅} ∧
  ∀e s. POW (e INSERT s) = (let ps = POW s in IMAGE ($INSERT e) ps ∪ ps)

⊢ ∀e s. POW (e INSERT s) = IMAGE ($INSERT e) (POW s) ∪ POW s

⊢ ∀set e. POW set e ⇔ e ⊆ set

⊢ ∀f s. PREIMAGE f s = s ∘ f

⊢ ∀f s. PREIMAGE f (BIGUNION s) = BIGUNION (IMAGE (PREIMAGE f) s)

⊢ ∀f g s. PREIMAGE f (PREIMAGE g s) = PREIMAGE (g ∘ f) s

⊢ ∀f s. PREIMAGE f (COMPL s) = COMPL (PREIMAGE f s)

⊢ ∀f t sp. PREIMAGE f (COMPL t) ∩ sp = sp DIFF PREIMAGE f t

⊢ ∀f a b. PREIMAGE f (a × b) = PREIMAGE (FST ∘ f) a ∩ PREIMAGE (SND ∘ f) b

⊢ ∀f s t. PREIMAGE f (s DIFF t) = PREIMAGE f s DIFF PREIMAGE f t

⊢ ∀f s t. DISJOINT s t ⇒ DISJOINT (PREIMAGE f s) (PREIMAGE f t)

⊢ ∀f. PREIMAGE f ∅ = ∅

⊢ PREIMAGE I = I ∧ PREIMAGE (λx. x) = (λx. x)

⊢ ∀f s. s ⊆ PREIMAGE f (IMAGE f s)

⊢ ∀f s t. PREIMAGE f (s ∩ t) = PREIMAGE f s ∩ PREIMAGE f t

⊢ ∀x s. PREIMAGE (K x) s = if x ∈ s then 𝕌(:β) else ∅

⊢ ∀f s t. s ⊆ t ⇒ PREIMAGE f s ⊆ PREIMAGE f t

⊢ ∀f s t. PREIMAGE f (s ∪ t) = PREIMAGE f s ∪ PREIMAGE f t

⊢ ∀f. PREIMAGE f 𝕌(:β) = 𝕌(:α)

⊢ ∀f s x. PREIMAGE f s x ⇔ f x ∈ s

⊢ ∀f g s. PREIMAGE (f ∘ g) s = PREIMAGE g (s ∘ f)

⊢ ∀s f1 f2. (∀x. x ∈ s ⇒ f1 x = f2 x) ⇒ Π f1 s = Π f2 s

⊢ ∀s. FINITE s ⇒ ∀c. Π (K c) s = c ** CARD s

⊢ ∀s. FINITE s ⇒
      ∀f e.
        0 < f e ⇒ Π f (s DELETE e) = if e ∈ s then Π f s DIV f e else Π f s

⊢ ∀f. Π f ∅ = 1

⊢ ∀s. FINITE s ⇒ (Π f s = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)

⊢ ∀s. FINITE s ⇒ (Π f s = 1 ⇔ IMAGE f s ⊆ {1})

⊢ ∀s. FINITE s ⇒ ∀f e. e ∉ s ⇒ Π f (e INSERT s) = f e * Π f s

⊢ ∀f. Π f ∅ = 1 ∧
      ∀e s. FINITE s ⇒ Π f (e INSERT s) = f e * Π f (s DELETE e)

⊢ PROD_SET ∅ = 1

⊢ ∀f s x.
    FINITE (IMAGE f s) ∧ f x ∉ IMAGE f s ⇒
    PROD_SET (IMAGE f (x INSERT s)) = f x * PROD_SET (IMAGE f s)

⊢ ∀x s. FINITE s ∧ x ∉ s ⇒ PROD_SET (x INSERT s) = x * PROD_SET s

⊢ PROD_SET ∅ = 1 ∧
  ∀x s. FINITE s ⇒ PROD_SET (x INSERT s) = x * PROD_SET (s DELETE x)

⊢ ∀s1 s2. s1 ⊂ s2 ⇔ s1 ⊆ s2 ∧ ¬(s2 ⊆ s1)

⊢ ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ FINITE t

⊢ ∀s t. s ⊂ t ⇔ ∃x. x ∉ s ∧ x INSERT s ⊆ t

⊢ ∀s. ¬(s ⊂ s)

⊢ ∀s t. s ⊂ t ⇔ s ⊆ t ∧ ∃y. y ∈ t ∧ y ∉ s

⊢ ∀s x. x ⊂ {s} ⇔ x = ∅

⊢ ∀s t u. s ⊂ t ∧ t ⊆ u ⇒ s ⊂ u

⊢ ∀s t u. s ⊂ t ∧ t ⊂ u ⇒ s ⊂ u

⊢ ∀s. s ⊂ 𝕌(:α) ⇔ ∃x. x ∉ s

⊢ RC $PSUBSET = $SUBSET

⊢ RC $SUBSET = $SUBSET

⊢ REL_RESTRICT R ∅ = ∅ᵣ

⊢ s1 ⊆ s2 ⇒ REL_RESTRICT R s1 ⊆ᵣ REL_RESTRICT R s2

⊢ ∀f g s t.
    IMAGE f s ⊆ t ⇒
    RESTRICTION s (RESTRICTION t g ∘ RESTRICTION s f) =
    RESTRICTION s (g ∘ f)

⊢ ∀f g s t.
    IMAGE f s ⊆ t ⇒
    RESTRICTION s (RESTRICTION t g ∘ f) = RESTRICTION s (g ∘ f)

⊢ ∀f g s. RESTRICTION s (g ∘ RESTRICTION s f) = RESTRICTION s (g ∘ f)

⊢ ∀s f g. RESTRICTION s f = RESTRICTION s g ⇔ ∀x. x ∈ s ⇒ f x = g x

⊢ ∀s f. RESTRICTION s f = f ⇔ f ∈ EXTENSIONAL s

⊢ ∀s f. RESTRICTION s (RESTRICTION s f) = RESTRICTION s f

⊢ ∀s f. RESTRICTION s f ∈ EXTENSIONAL s

⊢ ∀s t f. s ⊆ t ⇒ RESTRICTION s (RESTRICTION t f) = RESTRICTION s f

⊢ ∀s f g. RESTRICTION s f = g ⇔ EXTENSIONAL s g ∧ ∀x. x ∈ s ⇒ f x = g x

⊢ ∀s f g. f = RESTRICTION s g ⇔ EXTENSIONAL s f ∧ ∀x. x ∈ s ⇒ f x = g x

⊢ ∀s. s ≠ ∅ ⇒ REST s ⊂ s

⊢ ∀x. REST {x} = ∅

⊢ ∀s. REST s ⊆ s

⊢ ∀x s. REST s x ⇔ x ∈ s ∧ x ≠ CHOICE s

⊢ ∀f s t. SURJ f s t ⇒ ∀x. x ∈ t ⇒ f (RINV f s x) = x

⊢ $PSUBSET꙳ = $SUBSET

⊢ $SUBSET꙳ = $SUBSET

⊢ ∀s t. (∃f. INJ f s t) ∧ (∃g. INJ g t s) ⇒ ∃h. BIJ h s t

⊢ ∀s t. t ⊆ s ∧ (∃f. INJ f s t) ⇒ ∃g. BIJ g s t

⊢ ∀f s. x ∈ schroeder_close f s ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s

⊢ ∀f s. IMAGE f (schroeder_close f s) ⊆ schroeder_close f s

⊢ ∀f s t. f ∈ FUNSET s s ∧ t ⊆ s ⇒ schroeder_close f t ⊆ s

⊢ ∀f s. s ⊆ schroeder_close f s

⊢ ∀s. s = ∅ ∨ ∃x t. s = x INSERT t ∧ x ∉ t

⊢ ∀s t. s = t ⇔ s ⊆ t ∧ t ⊆ s

⊢ ∀s M. (∃x. x ∈ s) ⇔ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ M x ≤ M y

⊢ ∀n s. FINITE s ∧ (∀e. e ∈ s ⇒ CARD e = n) ⇒ ∑ CARD s = n * CARD s

⊢ ∀n s. FINITE s ∧ (∀e. e ∈ s ⇒ CARD e = n) ⇒ ∑ CARD s = n * CARD s

⊢ ∀s f1 f2. (∀x. x ∈ s ⇒ f1 x = f2 x) ⇒ ∑ f1 s = ∑ f2 s

⊢ ∀s. FINITE s ⇒ ∀f k. (∀x. x ∈ s ⇒ f x = k) ⇒ ∑ f s = k * CARD s

⊢ ∀s. FINITE s ⇒ ∀f g. (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ ∑ f s ≤ ∑ g s

⊢ ∀P. P ∅ ∧ (∀s. P s ⇒ ∀e. P (e INSERT s)) ⇒ ∀s. FINITE s ⇒ P s

⊢ ∀x. SING {x}

⊢ ∀s. SING s ⇒ CARD s = 1

⊢ ∀x. {x} DELETE x = ∅

⊢ ∀s. SING s ⇒ ∀x y. x ∈ s ∧ y ∈ s ⇒ x = y

⊢ SING ∅ ⇔ F

⊢ ∀s. SING s ⇒ FINITE s

⊢ ∀s. SING s ⇔ CARD s = 1 ∧ FINITE s

⊢ ∀s. SING s ⇔ s ≠ ∅ ∧ REST s = ∅

⊢ SING (x INSERT s) ⇔ s = ∅ ∨ s = {x}

⊢ ∀s x. {x} ∩ s = if x ∈ s then {x} else ∅

⊢ ∀s. s ≠ ∅ ⇒ (SING s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ x = y)

⊢ ∀s. SING s ⇔ s ≠ ∅ ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ x = y

⊢ SING (s ∪ t) ⇔ SING s ∧ t = ∅ ∨ SING t ∧ s = ∅ ∨ SING s ∧ SING t ∧ s = t

⊢ ∀x y. {y} x ⇔ x = y

⊢ ∀x w. {x} partitions w ⇔ x = w ∧ w ≠ ∅

⊢ ∀P x. x ∈ P ⇔ P x

⊢ ∀f n d. (∀n. f n ⊆ f (SUC n)) ⇒ f n ⊆ f (n + d)

⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇒ s = t

⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇔ s = t

⊢ ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y

⊢ ∀f g. f ⊆ g ⇒ BIGUNION f ⊆ BIGUNION g

⊢ ∀x P. x ∈ P ⇒ x ⊆ BIGUNION P

⊢ B ⊆ A ∧ A ∈ As ⇒ B ⊆ BIGUNION As

⊢ ∀f s t.
    FINITE s ∧ s ⊆ t ∧ closure_comm_assoc_fun f t ⇒
    ∀x b::t. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)

⊢ ∀f s t.
    FINITE s ∧ s ⊆ t ∧ closure_comm_assoc_fun f t ⇒
    ∀x b::t. ITSET f (x INSERT s) b = f x (ITSET f (s DELETE x) b)

⊢ ∀f s t.
    FINITE s ∧ s ⊆ t ∧ closure_comm_assoc_fun f t ⇒
    ∀x b::t. ITSET f s (f x b) = f x (ITSET f s b)

⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ a × c ⊆ b × d

⊢ ∀x s t. s ⊆ t DELETE x ⇔ x ∉ s ∧ s ⊆ t

⊢ ∀s1 s2 x. s1 ⊆ s2 ⇒ s1 DELETE x ⊆ s2 DELETE x

⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇔ s1 ⊆ s2 ∧ DISJOINT s1 s3

⊢ ∀s t. s DIFF t = ∅ ⇔ s ⊆ t

⊢ ∀s t u v. DISJOINT s t ∧ u ⊆ s ∧ v ⊆ t ⇒ DISJOINT u v

⊢ ∀s. s ⊆ ∅ ⇔ s = ∅

⊢ ∀s. FINITE s ⇒ ∀t. FINITE t ∧ CARD s = CARD t ∧ s ⊆ t ⇒ s = t

⊢ ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ FINITE t

⊢ ∀s t. FINITE s ∧ t ⊆ s ⇒ FINITE t

⊢ ∀f s t. s ⊆ IMAGE f t ⇔ ∃u. u ⊆ t ∧ s = IMAGE f u

⊢ ∀x s. x ∉ s ⇒ ∀t. s ⊆ x INSERT t ⇔ s ⊆ t

⊢ ∀x s t. s ⊆ x INSERT t ⇔ s DELETE x ⊆ t

⊢ ∀e s1 s2. s1 ⊆ s2 ⇒ s1 ⊆ e INSERT s2

⊢ ∀s t u. s ⊆ t ∩ u ⇔ s ⊆ t ∧ s ⊆ u

⊢ ∀s t. s ⊆ t ⇒ s ∩ t = s

⊢ ∀s t. s ⊆ t ⇒ t ∩ s = s

⊢ ∀s t. s ⊆ t ⇔ s ∩ t = s

⊢ ∀x y. x ⊆ K y ⇔ x ⊆ ∅ ∨ y

⊢ ∀I J. FINITE I ∧ FINITE J ∧ I ⊆ J ⇒ MAX_SET I ≤ MAX_SET J

⊢ ∀I J. I ≠ ∅ ∧ J ≠ ∅ ∧ I ⊆ J ⇒ MIN_SET J ≤ MIN_SET I

⊢ ∀x s. s ⊆ x INSERT s

⊢ ∀s1 s2. s1 ⊆ s2 ⇒ POW s1 ⊆ POW s2

⊢ ∀s t u. s ⊆ t ∧ t ⊂ u ⇒ s ⊂ u

⊢ ∀s. s ⊆ s

⊢ x ⊆ {a} ⇔ x = ∅ ∨ x = {a}

⊢ ∀P Q. P ⊆ Q ⇒ ∀x. x ∈ P ⇒ x ∈ Q

⊢ ∀s t u. s ⊆ t ∧ t ⊆ u ⇒ s ⊆ u

⊢ (∀s t. s ⊆ s ∪ t) ∧ ∀s t. s ⊆ t ∪ s

⊢ ∀s t. s ⊆ t ⇔ s ∪ t = t

⊢ ∀s. s ⊆ 𝕌(:α)

⊢ ∀s t. s ⊆ t ⇔ ∀x. s x ⇒ t x

⊢ FINITE s ⇒ s ⊆ count (MAX_SET s + 1)

⊢ reflexive $SUBSET

⊢ transitive $SUBSET

⊢ ∀s. FINITE s ⇒ ∑ (λx. f x + g x) s = ∑ f s + ∑ g s

⊢ s1 = s2 ∧ (∀x. x ∈ s2 ⇒ f1 x = f2 x) ⇒ ∑ f1 s1 = ∑ f2 s2

⊢ ∀s. FINITE s ⇒ ∀c. ∑ (K c) s = c * CARD s

⊢ ∀f s.
    FINITE s ⇒ ∀e. ∑ f (s DELETE e) = if e ∈ s then ∑ f s − f e else ∑ f s

⊢ ∀s t.
    FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒ ∀f. ∑ f (s ∪ t) = ∑ f s + ∑ f t

⊢ ∀f. ∑ f ∅ = 0

⊢ ∀s. FINITE s ⇒ ∀g. INJ g s 𝕌(:α) ⇒ ∀f. ∑ f (IMAGE g s) = ∑ (f ∘ g) s

⊢ ∀f s. FINITE s ⇒ ∀e. e ∉ s ⇒ ∑ f (e INSERT s) = f e + ∑ f s

⊢ ∀f s e. FINITE s ∧ e ∈ s ⇒ f e ≤ ∑ f s

⊢ ∀s. FINITE s ⇒
      (∃x. x ∈ s ∧ f x < g x) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
      ∑ f s < ∑ g s

⊢ ∀s. FINITE s ⇒ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ ∑ f s ≤ ∑ g s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀f g. (∀x. x ∈ s ⇒ f x < g x) ⇒ ∑ f s < ∑ g s

⊢ ∀s. FINITE s ⇒ ∀g. g PERMUTES s ⇒ ∀f. ∑ (f ∘ g) s = ∑ f s

⊢ ∀f e. ∑ f {e} = f e

⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ ∑ f t ≤ ∑ f s

⊢ ∀f. ∑ f ∅ = 0 ∧
      ∀e s. FINITE s ⇒ ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)

⊢ ∀f s t. FINITE s ∧ FINITE t ⇒ ∑ f (s ∪ t) = ∑ f s + ∑ f t − ∑ f (s ∩ t)

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ ∀f. ∑ f (s ∪ t) + ∑ f (s ∩ t) = ∑ f s + ∑ f t

⊢ ∀s. FINITE s ⇒ (∑ f s = 0 ⇔ ∀x. x ∈ s ⇒ f x = 0)

⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ n ≤ f x) ⇒ CARD s * n ≤ ∑ f s

⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ f x ≤ n) ⇒ ∑ f s ≤ CARD s * n

⊢ ∀P. FINITE P ⇒
      ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ f p = f q) ⇒ ∑ f P = CARD P * f p

⊢ ∀s. FINITE s ⇒
      ∀e. SUM_SET (s DELETE e) = if e ∈ s then SUM_SET s − e else SUM_SET s

⊢ SUM_SET ∅ = 0

⊢ ∀s x. FINITE s ∧ x ∉ s ⇒ SUM_SET (x INSERT s) = x + SUM_SET s

⊢ ∀x s. FINITE s ∧ x ∈ s ⇒ x ≤ SUM_SET s

⊢ ∀n. SUM_SET {n} = n

⊢ ∀s t. FINITE t ∧ s ⊆ t ⇒ SUM_SET s ≤ SUM_SET t

⊢ SUM_SET ∅ = 0 ∧
  ∀x s. FINITE s ⇒ SUM_SET (x INSERT s) = x + SUM_SET (s DELETE x)

⊢ ∀s t.
    FINITE s ∧ FINITE t ⇒
    SUM_SET (s ∪ t) = SUM_SET s + SUM_SET t − SUM_SET (s ∩ t)

⊢ SUM_SET (count n) = n * (n − 1) DIV 2

⊢ ∀n. 2 * SUM_SET (count n) = n * (n − 1)

⊢ 𝕌(:α + β) = IMAGE INL 𝕌(:α) ∪ IMAGE INR 𝕌(:β)

⊢ ∀s f.
    FINITE s ∧ IMAGE f s ⊆ s ⇒
    ((∀y. y ∈ s ⇒ ∃x. x ∈ s ∧ f x = y) ⇔
     ∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y)

⊢ ∀s t f.
    FINITE s ∧ FINITE t ∧ CARD s = CARD t ∧ IMAGE f s ⊆ t ⇒
    ((∀y. y ∈ t ⇒ ∃x. x ∈ s ∧ f x = y) ⇔
     ∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y)

⊢ ∀s. FINITE s ⇒ ∀t. SURJ f s t ⇒ FINITE t ∧ CARD t ≤ CARD s

⊢ ∀f g s t u. SURJ f s t ∧ SURJ g t u ⇒ SURJ (g ∘ f) s u

⊢ ∀f g s t. (∀x. x ∈ s ⇒ f x = g x) ⇒ (SURJ f s t ⇔ SURJ g s t)

⊢ ∀f s t x. SURJ f s t ∧ x ∈ s ⇒ f x ∈ t

⊢ ∀f. (∀s. SURJ f ∅ s ⇔ s = ∅) ∧ ∀s. SURJ f s ∅ ⇔ s = ∅

⊢ ∀s. SURJ (λx. x) s s

⊢ SURJ f s (IMAGE f s)

⊢ ∀s t. (∃f. SURJ f s t) ⇒ ∃g. INJ g t s

⊢ SURJ f s t ⇒ ∃g. INJ g t s ∧ ∀y. y ∈ t ⇒ f (g y) = y

⊢ $PSUBSET⁺ = $PSUBSET

⊢ $SUBSET⁺ = $SUBSET

⊢ ∀s t u. s ∪ (t ∪ u) = s ∪ t ∪ u

⊢ ∀s t. s ∪ t = t ∪ s

⊢ ∀n. count n ∪ from n = 𝕌(:num)

⊢ ∀A B x. A ∪ B DELETE x = A DELETE x ∪ (B DELETE x)

⊢ s ⊆ t ⇒ s ∪ (t DIFF s) = t ∧ t DIFF s ∪ s = t

⊢ ∀s t. s ∪ (s DIFF t) = s

⊢ (∀s t. s ∪ (t DIFF s) = s ∪ t) ∧ ∀s t. t DIFF s ∪ s = t ∪ s

⊢ (∀s. ∅ ∪ s = s) ∧ ∀s. s ∪ ∅ = s

⊢ ∀n. from n ∪ count n = 𝕌(:num)

⊢ ∀s. s ∪ s = s

⊢ ∀s t u. s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

⊢ ∀s t u. s ∪ t ⊆ u ⇔ s ⊆ u ∧ t ⊆ u

⊢ (∀s. 𝕌(:α) ∪ s = 𝕌(:α)) ∧ ∀s. s ∪ 𝕌(:α) = 𝕌(:α)

⊢ ∀s t x. (s ∪ t) x ⇔ x ∈ s ∨ x ∈ t

⊢ ∀x s. x ∈ s ∧ (∀y. y ∈ s ⇒ x = y) ⇔ s = {x}

⊢ 𝕌(:bool) = {T; F}

⊢ FUNSET 𝕌(:α) 𝕌(:β) = 𝕌(:α -> β)

⊢ 𝕌(:α -> bool) = POW 𝕌(:α)

⊢ 𝕌(:α) ≠ ∅

⊢ ∀s. 𝕌(:α) ⊆ s ⇔ s = 𝕌(:α)

⊢ ∀x. 𝕌(:α) x

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s

⊢ ∀s. countable s ∧ (∀x. x ∈ s ⇒ countable x) ⇒ countable (BIGUNION s)

⊢ (∀s. chooser s 0 = CHOICE s) ∧
  (∀s n.
     chooser s <..num comp'n..> = chooser (REST s) (<..num comp'n..> − 1)) ∧
  ∀s n. chooser s <..num comp'n..> = chooser (REST s) <..num comp'n..>

⊢ ∀s x. COMPL (x INSERT s) = COMPL s DELETE x

⊢ ∀n. count n = if n = 0 then ∅ else (let p = PRE n in p INSERT count p)

⊢ ∀n m. count (n + m) = count n ∪ IMAGE ($+ n) (count m)

⊢ ∀n. count (n + 1) = n INSERT count n

⊢ countable ∅

⊢ countable (x INSERT s) ⇔ countable s

⊢ countable 𝕌(:α # β) ⇔ countable 𝕌(:α) ∧ countable 𝕌(:β)

⊢ countable 𝕌(:α + β) ⇔ countable 𝕌(:α) ∧ countable 𝕌(:β)

⊢ countable (IMAGE f 𝕌(:num))

⊢ ∀s. countable s ⇔ s = ∅ ∨ ∃f. SURJ f 𝕌(:num) s

⊢ ∀s t. countable s ∧ countable t ⇒ countable (s × t)

⊢ countable (s × t) ⇔ s = ∅ ∨ t = ∅ ∨ countable s ∧ countable t

⊢ x ⊔ y = ∅ ⇔ x = ∅ ∧ y = ∅

⊢ 𝕌(:α + β) = 𝕌(:α) ⊔ 𝕌(:β)

⊢ ∀A a b. disjoint A ⇒ a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b

⊢ ∀A. (∀a b. a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b) ⇒ disjoint A

⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ DISJOINT a b

⊢ disjoint ∅

⊢ ∀f. (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒ disjoint (IMAGE f 𝕌(:α))

⊢ ∀e c. disjoint c ∧ (∀x. x ∈ c ⇒ DISJOINT x e) ⇒ disjoint (e INSERT c)

⊢ ∀e c. disjoint (e INSERT c) ⇒ disjoint c

⊢ ∀e c. disjoint (e INSERT c) ∧ e ∉ c ⇒ ∀s. s ∈ c ⇒ DISJOINT e s

⊢ ∀e c. disjoint c ⇒ disjoint (IMAGE ($INTER e) c)

⊢ ∀s t. s = t ⇒ disjoint {s; t}

⊢ ∀a. disjoint {a}

⊢ ∀s t. s ≠ t ∧ DISJOINT s t ⇒ disjoint {s; t}

⊢ ∀A B.
    disjoint A ∧ disjoint B ∧ BIGUNION A ∩ BIGUNION B = ∅ ⇒
    disjoint (A ∪ B)

⊢ ∀s. ∅ partitions s ⇔ s = ∅

⊢ ∀v. ∅ refines v

⊢ ∀R s x y.
    R equiv_on s ∧ x ∈ s ∧ y ∈ s ⇒
    (equiv_class R s x = equiv_class R s y ⇔ R x y)

⊢ ∀R s t. R equiv_on s ∧ t ⊆ s ⇒ R equiv_on t

⊢ equivalence (λx y. part v x = part v y)

⊢ ∀s. FINITE s ⇒ countable s

⊢ ∀f s. countable s ⇒ countable (IMAGE f s)

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s

⊢ ∀w v x. v partitions w ∧ x ∈ w ⇒ x ∈ part v x

⊢ ∀s. INFINITE s ⇔ ∃f. INJ f 𝕌(:num) s

⊢ ∀s. INFINITE s ⇒ ¬countable (POW s)

⊢ ∀s. INFINITE s ⇒ INFINITE (REST s)

⊢ ∀f s t. countable t ∧ INJ f s t ⇒ countable s

⊢ INJ f s (IMAGE f s) ⇒ (countable (IMAGE f s) ⇔ countable s)

⊢ ∀f s t. INJ f s t ⇒ s = ∅ ∨ ∃f'. SURJ f' t s

⊢ ∀s t. countable s ∨ countable t ⇒ countable (s ∩ t)

⊢ ∀R Y f. R equiv_on Y ⇒ inv_image R f equiv_on {x | f x ∈ Y}

⊢ ∀x s m e y.
    x ∈ s ∧ m e < m x ⇒
    (is_measure_maximal m (e INSERT s) y ⇔ is_measure_maximal m s y)

⊢ is_measure_maximal m {x} y ⇔ y = x

⊢ ∀s. FINITE s ⇔ ∃a. ∀x. x ∈ s ⇒ x ≤ a

⊢ ∀s. FINITE s ⇒ ∃a. a ∉ s

⊢ INFINITE 𝕌(:num)

⊢ countable 𝕌(:num)

⊢ ∀x y. pair_to_num (x,y) = (x + y + 1) * (x + y) DIV 2 + y

⊢ (∀x. pair_to_num (num_to_pair x) = x) ∧
  ∀x y. num_to_pair (pair_to_num (x,y)) = (x,y)

⊢ (∀x. pair_to_num (num_to_pair x) = x) ∧
  ∀x. num_to_pair (pair_to_num x) = x

⊢ ∀r. pairwise r ∅

⊢ ∀R s t. pairwise R t ∧ s ⊆ t ⇒ pairwise R s

⊢ pairwise R (s1 ∪ s2) ⇔
  pairwise R s1 ∧ pairwise R s2 ∧ ∀x y. x ∈ s1 ∧ y ∈ s2 ⇒ R x y ∧ R y x

⊢ ∀x w. x ∈ w ⇒ part {w} x = w

⊢ ∀w v x. v partitions w ∧ x ∈ w ⇒ part v x ∈ v

⊢ ∀R w y.
    y ∈ w ∧ R equiv_on w ⇒ part (partition R w) y = {x | x ∈ w ∧ R x y}

⊢ ∀w v x s. v partitions w ∧ x ∈ w ∧ x ∈ s ∧ s ∈ v ⇒ s = part v x

⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ CARD s = ∑ CARD (partition R s)

⊢ ∀R s t. t ∈ partition R s ⇒ t ⊆ s

⊢ R equiv_on s ⇒
  ∀t1 t2.
    t1 ∈ partition R s ∧ t2 ∈ partition R s ∧ t1 ≠ t2 ⇒ DISJOINT t1 t2

⊢ R equiv_on s ⇒ ∀t. t ∈ partition R s ⇒ ∀x y. x ∈ t ∧ y ∈ t ⇒ R x y

⊢ ∀R1 R2 Y.
    R1 equiv_on Y ∧ R2 equiv_on Y ∧ partition R1 Y = partition R2 Y ⇒
    ∀x y. x ∈ Y ∧ y ∈ Y ⇒ (R1 x y ⇔ R2 x y)

⊢ ∀v w s1 s2. v partitions w ∧ s1 ∈ v ∧ s2 ∈ v ∧ s1 ≠ s2 ⇒ DISJOINT s1 s2

⊢ ∀X Y. X partitions Y ∧ FINITE Y ⇒ FINITE X ∧ ∀s. s ∈ X ⇒ FINITE s

⊢ ∀x w v.
    x ∉ w ⇒
    (v partitions x INSERT w ⇔
     ∃u s.
       u partitions w ∧ v = (x INSERT s) INSERT u DELETE s ∧
       (s ≠ ∅ ⇒ s ∈ u))

⊢ ∀x y.
    x partitions y ⇔
    ∅ ∉ x ∧ (∀s t. s ∈ x ∧ t ∈ x ∧ s ≠ t ⇒ DISJOINT s t) ∧ BIGUNION x = y

⊢ ∀v x. SING x ⇒ (v partitions x ⇔ v = {{CHOICE x}})

⊢ ∀x y. x partitions y ⇒ BIGUNION x = y

⊢ ∀v. v partitions ∅ ⇔ v = ∅

⊢ ∀x w1 w2. x partitions w1 ∧ x partitions w2 ⇒ w1 = w2

⊢ ∀X Y.
    X partitions Y ⇔
    (∀x. x ∈ X ⇒ x ≠ ∅ ∧ x ⊆ Y) ∧ ∀y. y ∈ Y ⇒ ∃!x. x ∈ X ∧ y ∈ x

⊢ ∀s. ¬∃f. SURJ f s (POW s)

⊢ ∀f s.
    FINITE s ⇒
    (prime (Π f s) ⇔
     ∃p. IMAGE f s ⊆ {1; p} ∧ prime p ∧ ∃!x. x ∈ s ∧ f x = p)

⊢ ∀w v1 v2.
    v1 partitions w ∧ v2 partitions w ∧ v1 refines v2 ∧ v2 refines v1 ⇒
    v1 = v2

⊢ ∀w v1 v2.
    v1 partitions w ∧ v2 partitions w ⇒
    (v1 refines v2 ⇔
     ∀x y. x ∈ w ∧ y ∈ w ∧ part v1 x = part v1 y ⇒ part v2 x = part v2 y)

⊢ ∀v. v refines v

⊢ ∀v1 v2 v3. v1 refines v2 ∧ v2 refines v3 ⇒ v1 refines v3

⊢ ∀s t. countable s ∧ t ⊆ s ⇒ countable t

⊢ transitive $PSUBSET

⊢ ∀s t. countable s ∧ countable t ⇒ countable (s ∪ t)

⊢ countable (s ∪ t) ⇔ countable s ∧ countable t