Theory cardinal

⊢ A × BIGPROD As ≈ BIGPROD (IMAGE INL A INSERT IMAGE (IMAGE INR) As)

⊢ BIGPROD As = ∅ ⇔ ∅ ∈ As

⊢ BIGPROD ∅ ≈ {()}

⊢ BIGPROD {A} ≈ A

⊢ ∀A. BIGPROD A = BIGPRODi (λa. if a ∈ A then SOME a else NONE)

⊢ A1 ≠ A2 ⇒ BIGPROD {A1; A2} ≈ A1 × A2

⊢ BIGPROD A =
  {tup |
   (∀s. s ∈ A ⇒ ∃a. tup s = SOME a ∧ a ∈ s) ∧ ∀s. s ∉ A ⇒ tup s = NONE}

⊢ (∀i. Af i ≠ SOME ∅) ∧ (∀i. Bf i ≠ SOME ∅) ⇒
  (BIGPRODi Af = BIGPRODi Bf ⇔ Af = Bf)

⊢ BIGPRODi Af = ∅ ⇔ ∃i. Af i = SOME ∅

⊢ BIGPRODi (K NONE) = {K NONE}

⊢ BIGPRODi (fnOfSet {(i,s)}) ≈ s

⊢ BIGPRODi (fnOfSet {(i,s)}) = {(K NONE)⦇i ↦ SOME a⦈ | a ∈ s}

⊢ ∀A. BIGPRODi A =
      {tup |
       (∀i. A i = NONE ⇒ tup i = NONE) ∧
       ∀i s. A i = SOME s ⇒ ∃a. tup i = SOME a ∧ a ∈ s}

⊢ i ≠ j ⇒ BIGPRODi (K NONE)⦇i ↦ SOME A1; j ↦ SOME A2⦈ ≈ A1 × A2

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

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

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

⊢ A ≺ POW A

⊢ ∀s. s ≺ {t | t ⊆ s}

⊢ 𝕌(:α) ≺ 𝕌(:α -> bool)

⊢ A ≈ {()} ⇔ ∃a. A = {a}

⊢ (x ≈ ∅ ⇔ x = ∅) ∧ (∅ ≈ x ⇔ x = ∅)

⊢ s1 ≈ s2 ∧ FINITE s1 ⇒ CARD s1 = CARD s2

⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ (s1 ≼ t1 ⇔ s2 ≼ t2)

⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≈ s2 ⇔ CARD s1 = CARD s2)

⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ s1 × t1 ≈ s2 × t2

⊢ {x} × A ≈ A ∧ A × {x} ≈ A

⊢ s × t ≈ t × s

⊢ ∀s t. s ∩ t = ∅ ⇒ s ∪ t ≈ s ⊔ t

⊢ s1 ≈ s2 ⇒ (FINITE s1 ⇔ FINITE s2)

⊢ ∀s. INFINITE s ⇒ x INSERT s ≈ s

⊢ s ≈ t ⇒ s ≼ t

⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≼ s2 ⇔ CARD s1 ≤ CARD s2)

⊢ ∀x1 x2 y1 y2. x1 ≼ x2 ∧ y1 ≼ y2 ⇒ x1 × y1 ≼ x2 × y2

⊢ ∀s1 s2. FINITE s2 ∧ s1 ≼ s2 ⇒ FINITE s1

⊢ {()} ≺ 𝟚 ∧ {()} ≉ 𝟚 ∧ 𝟚 ≉ {()} ∧ {()} ≼ 𝟚

⊢ ∀s t u. INFINITE u ∧ s ≼ u ∧ t ≼ u ⇒ s ⊔ t ≼ u

⊢ ∀s t u. INFINITE u ∧ s ≺ u ∧ t ≺ u ⇒ s ⊔ t ≺ u

⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s ⊔ t ≈ t

⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s ⊔ t ≼ t

⊢ ∀s t u. s ⊔ (t ⊔ u) ≈ s ⊔ t ⊔ u

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

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ s ⊔ t ≈ s' ⊔ t'

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE (s ⊔ t)

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

⊢ ∀s. INFINITE s ⇒ s ⊔ s ≼ s × s

⊢ ∀s t. s ⊔ t ≈ t ⊔ s

⊢ INFINITE k ∧ s1 ≼ k ∧ (∀e. e ∈ s1 ⇒ e ≼ k) ⇒ BIGUNION s1 ≼ k

⊢ ∀s t m n.
    s HAS_SIZE m ∧ (∀x. x ∈ s ⇒ FINITE (t x) ∧ CARD (t x) ≤ n) ⇒
    CARD (BIGUNION {t x | x ∈ s}) ≤ m * n

⊢ CARD 𝕌(:bool) = 2

⊢ FINITE s1 ∧ FINITE s2 ∧ CARD s1 = CARD s2 ⇒ s1 ≈ s2

⊢ ∀s t. s ≈ t ⇒ (countable s ⇔ countable t)

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

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

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

⊢ ∀s1 s2. FINITE s1 ∧ FINITE s2 ⇒ (s1 ≈ s2 ⇔ CARD s1 = CARD s2)

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

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≈ t ⇔ s' ≈ t')

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

⊢ x ≈ ∅ ⇔ x = ∅

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

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

⊢ s ≈ t ⇒ s ≼ t

⊢ ∀s. s ≈ s

⊢ ∀s t. s ≈ t ⇔ t ≈ s

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

⊢ ∀s t.
    INFINITE t ∧ 𝕌(:bool) ≼ s ∧ s ≼ set_exp 𝕌(:bool) t ⇒
    set_exp s t ≈ set_exp 𝕌(:bool) t

⊢ ∀s. s ≺ set_exp 𝕌(:bool) s

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ set_exp s t ≈ set_exp s' t'

⊢ ∀s t u. set_exp s (t × u) ≈ set_exp (set_exp s t) u

⊢ ∀s. set_exp 𝕌(:bool) s ≈ {t | t ⊆ s}

⊢ ∀s b. set_exp s {b} ≈ s

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

⊢ ∀s t. s ≈ t ⇒ (FINITE s ⇔ FINITE t)

⊢ ∀s t n. s HAS_SIZE n ∧ s ≈ t ⇒ t HAS_SIZE n

⊢ ∀s t. s ≈ t ⇒ (INFINITE s ⇔ INFINITE t)

⊢ ∀s t u. s × (t ⊔ u) ≈ s × t ⊔ s × u

⊢ ∀s t. s ≼ t ∨ t ≺ s

⊢ ∀r s t. r ≼ s ∧ s ≺ t ⇒ r ≺ t

⊢ ∀s s' t t'. s ≼ s' ∧ t ≼ t' ⇒ s ⊔ t ≼ s' ⊔ t'

⊢ ∀s t. t ≼ s ⊔ t

⊢ ∀s t. s ≼ s ⊔ t

⊢ ∀s t. s ≼ t ∧ t ≼ s ⇔ s ≈ t

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s ≼ t ⇔ CARD s ≤ CARD t)

⊢ ∀s t. FINITE t ∧ s ≼ t ⇒ CARD s ≤ CARD t

⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ (s1 ≼ t1 ⇔ s2 ≼ t2)

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

⊢ ∀x. x ≼ ∅ ⇔ x = ∅

⊢ ∀s t. s ≼ t ⇔ ∃u. u ⊆ t ∧ s ≈ u

⊢ 𝟚 ≼ B ⇒ A ≼ set_exp B A

⊢ ∀s s' t. s ≼ s' ⇒ set_exp s t ≼ set_exp s' t

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

⊢ ∀f s. IMAGE f s ≼ s

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

⊢ ∀s t. INFINITE s ∧ s ≼ t ⇒ INFINITE t

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

⊢ ∀s1 s2. s1 ≼ s2 ⇔ s1 ≺ s2 ∨ s1 ≈ s2

⊢ ∀x1 x2 y1 y2. x1 ≼ x2 ∧ y1 ≼ y2 ⇒ x1 × y1 ≼ x2 × y2

⊢ ∀s. s ≼ s

⊢ ∀R s.
    (∀x y y'. x ∈ s ∧ R x y ∧ R x y' ⇒ y = y') ⇒
    {y | ∃x. x ∈ s ∧ R x y} ≼ s

⊢ ∀s. s ≼ s × s

⊢ ∀x y. x ⊆ y ⇒ x ≼ y

⊢ ∀s t. s ≼ t ∨ t ≼ s

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

⊢ ∀s. s ≼ 𝕌(:α)

⊢ ∀s t. s ≺ t ∨ t ≼ s

⊢ ∀r s t. r ≺ s ∧ s ≼ t ⇒ r ≺ t

⊢ ∀s s' t t'. s ≺ s' ∧ t ≺ t' ⇒ s ⊔ t ≺ s' ⊔ t'

⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≺ s2 ⇔ CARD s1 < CARD s2)

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≺ t ⇔ s' ≺ t')

⊢ ∀s t. FINITE s ∧ INFINITE t ⇒ s ≺ t

⊢ ∀s t. s ≺ t ⇒ s ≼ t

⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ s ≉ t

⊢ ∀s. ¬(s ≺ s)

⊢ ∀s t. s ≈ t ∨ s ≺ t ∨ t ≺ s

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

⊢ ∀s t u. INFINITE u ∧ s ≼ u ∧ t ≼ u ⇒ s × t ≼ u

⊢ ∀s t. INFINITE t ∧ s ≠ ∅ ∧ s ≼ t ⇒ s × t ≈ t

⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s × t ≼ t

⊢ ∀s t u. s × t × u ≈ (s × t) × u

⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ s1 × t1 ≈ s2 × t2

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

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

⊢ ∀s t. s ≺ t ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u

⊢ ∀s t. s ≼ t ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u

⊢ s × t ≈ t × s

⊢ ∀s t. t ≺ s ⇔ t ≺ s

⊢ ∀s t. ¬(s ≺ t) ⇔ t ≼ s

⊢ ∀s t u. (s ⊔ t) × u ≈ s × u ⊔ t × u

⊢ ∀s. INFINITE s ⇒ s × s ≈ s

⊢ 𝕌(:num) × 𝕌(:num) ≈ 𝕌(:num)

⊢ ∀a b. FINITE b ∧ a ⊆ b ∧ CARD a = CARD b ⇒ a = b

⊢ ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r

⊢ ∀t. countable t ⇔ 𝕌(:num) ≽ t

⊢ ∀s. countable s ⇔ s ≼ 𝕌(:num)

⊢ ∀s. countable s ∧ s ≠ ∅ ⇒ ∃f. s = IMAGE f 𝕌(:num)

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

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

⊢ ∀s. countable s ∧ INFINITE s ⇒
      ∃f. s = IMAGE f 𝕌(:num) ∧ ∀m n. f m = f n ⇒ m = n

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

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

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

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

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

⊢ countable ∅

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

⊢ ∀f A. (∀x y. f x = f y ⇒ x = y) ∧ countable A ⇒ countable {x | f x ∈ A}

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

⊢ ∀f A s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ countable A ⇒
    countable {x | x ∈ s ∧ f x ∈ A}

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

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

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

⊢ ∀s P. countable s ⇒ countable {x | x ∈ s ∧ P x}

⊢ ∀x. countable {x}

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

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

⊢ ∅ ≼ t

⊢ set_exp A ∅ = {K ARB} ∧ (B ≠ ∅ ⇒ set_exp ∅ B = ∅)

⊢ set_exp A ∅ ≈ count 1

⊢ ∀s t.
    s ≈ t ⇔
    ∃R. (∀x y. R (x,y) ⇒ x ∈ s ∧ y ∈ t) ∧
        (∀x. x ∈ s ⇒ ∃!y. y ∈ t ∧ R (x,y)) ∧
        ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ R (x,y)

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

⊢ (∀P f. (∃z. z ∈ {f x | P x} ∧ Q z) ⇔ ∃x. P x ∧ Q (f x)) ∧
  (∀P f. (∃z. z ∈ {f x y | P x y} ∧ Q z) ⇔ ∃x y. P x y ∧ Q (f x y)) ∧
  ∀P f. (∃z. z ∈ {f w x y | P w x y} ∧ Q z) ⇔ ∃w x y. P w x y ∧ Q (f w x y)

⊢ FINITE A ⇒ A = ∅ ∨ A ≈ {()} ∨ 2 ≤ CARD A

⊢ FINITE 𝕌(:bool)

⊢ ∀s. FINITE s ⇔ s ≺ 𝕌(:num)

⊢ FINITE s ∧ INFINITE t ⇒ s ≼ t

⊢ FINITE B ⇒ (countable (set_exp A B) ⇔ B = ∅ ∨ countable A)

⊢ FINITE B ∧ B ≠ ∅ ∧ ¬countable A ⇒ ¬countable (set_exp A B)

⊢ ∀f A. (∀x y. f x = f y ⇒ x = y) ∧ FINITE A ⇒ FINITE {x | f x ∈ A}

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

⊢ ∀s. FINITE s ⇒ countable s

⊢ FINITE (set_exp A B) ⇔ B = ∅ ∨ A ≼ {()} ∨ FINITE A ∧ FINITE B

⊢ (∀d. countable d ⇒ P d) ⇔ P ∅ ∧ ∀f. P (IMAGE f 𝕌(:num))

⊢ (∀P f. (∀z. z ∈ {f x | P x} ⇒ Q z) ⇔ ∀x. P x ⇒ Q (f x)) ∧
  (∀P f. (∀z. z ∈ {f x y | P x y} ⇒ Q z) ⇔ ∀x y. P x y ⇒ Q (f x y)) ∧
  ∀P f. (∀z. z ∈ {f w x y | P w x y} ⇒ Q z) ⇔ ∀w x y. P w x y ⇒ Q (f w x y)

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

⊢ 𝕌(:bool) HAS_SIZE 2

⊢ ∀s. (s HAS_SIZE 0 ⇔ s = ∅) ∧
      (s HAS_SIZE SUC n ⇔ ∃a t. t HAS_SIZE n ∧ a ∉ t ∧ s = a INSERT t)

⊢ ∀f s. IMAGE f s ≼ s

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

⊢ ∀p q r. p ∧ q ⇒ r ⇔ q ⇒ p ⇒ r

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

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

⊢ ∀s. INFINITE s ⇒ s ≠ ∅

⊢ INFINITE 𝕌(:num + α)

⊢ INFINITE A ⇔ 𝕌(:num) ≼ A

⊢ INFINITE A ⇒ (x INSERT s ≼ A ⇔ s ≼ A)

⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇔ ∀x y. f x = f y ⇔ x = y

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

⊢ (∀x y. f x = f y ⇒ x = y) ⇔ ∃g. ∀x. g (f x) = x

⊢ ∀P f.
    (∀x y. P x ∧ P y ∧ f x = f y ⇒ x = y) ⇔
    ∀x y. P x ∧ P y ⇒ (f x = f y ⇔ x = y)

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

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

⊢ ∀p q.
    p ∩ q = q ∩ p ∧ p ∩ q ∩ r = p ∩ q ∩ r ∧ p ∩ q ∩ r = q ∩ p ∩ r ∧
    p ∩ p = p ∧ p ∩ p ∩ q = p ∩ q

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

⊢ ∀s t x y. (x,y) ∈ s × t ⇔ x ∈ s ∧ y ∈ t

⊢ ∀P a b. (a,b) ∈ {(x,y) | P x y} ⇔ P a b

⊢ ∀P Q. (∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q

⊢ ∀P Q. (∀x. P x) ⇒ Q ⇔ ∃x. P x ⇒ Q

⊢ ∀s t. s ≼ t ⇔ ∃g. ∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ g y = x

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

⊢ countable 𝕌(:num)

⊢ INFINITE A ⇒ POW A ≈ set_exp A A

⊢ POW A ≈ set_exp (count 2) A

⊢ ∀P Q. P ⇒ (∃x. Q x) ⇔ ∃x. P ⇒ Q x

⊢ ∀P Q. P ⇒ (∀x. Q x) ⇔ ∀x. P ⇒ Q x

⊢ ∀s. INFINITE s ⇒ s × s ≈ s

⊢ INFINITE s ⇒ s ≈ 𝟚 × s ∧ ∀A B. DISJOINT A B ∧ A ≈ s ∧ B ≈ s ⇒ A ∪ B ≈ s

⊢ ∀s x. {x} ⊆ s ⇔ x ∈ s

⊢ set_exp {x} B = {(λb. if b ∈ B then x else ARB)} ∧
  set_exp A {x} = {(λb. if b = x then a else ARB) | a ∈ A}

⊢ set_exp {x} B ≈ count 1 ∧ set_exp A {x} ≈ A

⊢ ∀x y. x ⊆ y ⇒ x ≼ y

⊢ ∀f. (∀t. ∃s. IMAGE f s = t) ⇔ ∀y. ∃x. f x = y

⊢ ∀f. (∀y. ∃x. f x = y) ⇔ ∀P. IMAGE f {x | P (f x)} = {x | P x}

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

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

⊢ (∀y. ∃x. f x = y) ⇔ ∃g. ∀y. f (g y) = y

⊢ ∀s t. ¬countable s ∧ countable t ⇒ ¬countable (s DIFF t)

⊢ ∀s t. ¬countable s ∧ FINITE t ⇒ ¬countable (s DIFF t)

⊢ ∀p q.
    p ∪ q = q ∪ p ∧ p ∪ q ∪ r = p ∪ q ∪ r ∧ p ∪ q ∪ r = q ∪ p ∪ r ∧
    p ∪ p = p ∧ p ∪ p ∪ q = p ∪ q

⊢ ∀s t. s ∪ t ≼ s ⊔ t

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

⊢ INFINITE s ⇒ bijns s ≈ POW s

⊢ ∀f s. f ∈ bijns s ⇔ f permutes s

⊢ ∀A. bijns A = {f | f PERMUTES A ∧ ∀a. a ∉ A ⇒ f a = a}

⊢ x INSERT s ≈ s ⇔ x ∈ s ∨ INFINITE s

⊢ ∀s. s ≈ s

⊢ ∀s t. s ≈ t ⇔ t ≈ s

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

⊢ INFINITE 𝕌(:α) ⇒ 𝕌(:num + α) ≈ 𝕌(:α)

⊢ A ≈ B ⇒ bijns A ≈ bijns B

⊢ ∀s1 s2. s1 ≈ s2 ⇔ ∃f. BIJ f s1 s2

⊢ ∀s t. s ≽ t ⇔ t ≼ s

⊢ ∀s t. s ≻ t ⇔ t ≺ s

⊢ ∀s t. s ≼ t ∧ t ≼ s ⇒ s ≈ t

⊢ ∀s t. s ≼ t ∧ t ≼ s ⇔ s ≈ t

⊢ ∀s. s ≼ s

⊢ A ≼ B ⇔ (∃f. SURJ f B A) ∨ A = ∅

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

⊢ 𝕌(:α) ≼ 𝕌(:β) ⇒ ∀w1. ∃w2. orderiso w1 w2

⊢ ∀s1 s2. s1 ≼ s2 ⇔ ∃f. INJ f s1 s2

⊢ ∀s t. s ≼ t ∨ t ≼ s

⊢ ∀x. x ≼ ∅ ⇔ x = ∅

⊢ ∀r s t. r ≼ s ∧ s ≺ t ⇒ r ≺ t

⊢ ∀s1 s2. s1 ≼ s2 ⇔ s1 ≺ s2 ∨ s1 ≈ s2

⊢ x ≼ set_exp x e ⇔ x = ∅ ∨ x ≈ {()} ∨ e ≠ ∅

⊢ ∀s. ¬(s ≺ s)

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

⊢ A ≺ B ⇒ A ≼ B

⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ s ≉ t

⊢ ∀r s t. r ≺ s ∧ s ≼ t ⇒ r ≺ t

⊢ count n ≼ A ⇔ FINITE A ⇒ n ≤ CARD A

⊢ ∀s t. s ≈ t ⇒ (countable s ⇔ countable t)

⊢ countable (set_exp A B) ⇔
  B = ∅ ∨ FINITE B ∧ countable A ∨ A ≈ {()} ∨ A = ∅

⊢ ∀s. countable s ⇔ s ≼ 𝕌(:num)

⊢ ∀s. INFINITE s ⇒
      ∃A. BIGUNION A = s ∧ (∀a. a ∈ A ⇒ INFINITE a ∧ countable a) ∧
          ∀a1 a2. a1 ∈ A ∧ a2 ∈ A ∧ a1 ≠ a2 ⇒ DISJOINT a1 a2

⊢ ∀s. INFINITE s ⇒
      ∃A. BIGUNION A = s ∧ (∀a. a ∈ A ⇒ INFINITE a ∧ countable a) ∧
          pairwise (RC DISJOINT) A

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

⊢ e ∉ s ⇒ set_exp A (e INSERT s) ≈ A × set_exp A s

⊢ ∀s t. set_exp s t = {f | (∀x. x ∈ t ⇒ f x ∈ s) ∧ ∀x. x ∉ t ⇒ f x = ARB}

⊢ INFINITE A ∧ 0 < n ⇒ set_exp A (count n) ≈ A

⊢ INFINITE A ⇒ A ≈ {s | FINITE s ∧ s ⊆ A}

⊢ fnOfSet {(k,v)} = (K NONE)⦇k ↦ SOME v⦈

⊢ ∀s k. fnOfSet s k = if ∃!v. (k,v) ∈ s then SOME (@v. (k,v) ∈ s) else NONE

⊢ ∀s t. s ≽ t ⇔ t ≼ s

⊢ ∀s t. s ≻ t ⇔ t ≺ s

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

⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ s ≺ t

⊢ ∀s t. s × t = {(x,y) | x ∈ s ∧ y ∈ t}

⊢ (A ∪ B) × (A ∪ B) = A × A ∪ A × B ∪ B × A ∪ B × B

⊢ a1 ≈ a2 ⇒ b1 ≈ b2 ⇒ set_exp a1 b1 ≈ set_exp a2 b2

⊢ (b = ∅ ⇒ d = ∅) ⇒ a ≼ b ∧ c ≼ d ⇒ set_exp a c ≼ set_exp b d

⊢ ∀A B.
    set_exp A B =
    {f | (∀b. b ∈ B ⇒ ∃a. a ∈ A ∧ f b = a) ∧ ∀b. b ∉ B ⇒ f b = ARB}

⊢ set_exp (set_exp A B1) B2 ≈ set_exp A (B1 × B2)

⊢ set_exp A B = ∅ ⇔ A = ∅ ∧ B ≠ ∅

⊢ tup ∈ BIGPRODi Af ⇒ (tup i = NONE ⇔ Af i = NONE)

⊢ wellorder (destWO r)