Proofgold Address

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param Sep^Sep : ι → (ι → ο) → ι
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known Sep_In_Power^Sep_In_Power : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ∈ prim4 x0
Theorem KnasterTarski_set^{KnasterTarski_set} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ prim4 x0 ⟶ x1 x2 ∈ prim4 x0) ⟶ (∀ x2 . x2 ∈ prim4 x0 ⟶ ∀ x3 . x3 ∈ prim4 x0 ⟶ x2 ⊆ x3 ⟶ x1 x2 ⊆ x1 x3) ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ prim4 x0) (x1 x3 = x3) ⟶ x2) ⟶ x2 (proof)
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem image_In_Power^{image_In_Power} : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ ∀ x3 . x3 ∈ prim4 x0 ⟶ prim5 x3 x2 ∈ prim4 x1 (proof)
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem image_monotone^{image_monotone} : ∀ x0 : ι → ι . ∀ x1 x2 . x1 ⊆ x2 ⟶ prim5 x1 x0 ⊆ prim5 x2 x0 (proof)
Param setminus^setminus : ι → ι → ι
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Theorem setminus_In_Power^{setminus_In_Power} : ∀ x0 x1 . setminus x0 x1 ∈ prim4 x0 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Theorem setminus_antimonotone^{setminus_antimonotone} : ∀ x0 x1 x2 . x1 ⊆ x2 ⟶ setminus x0 x2 ⊆ setminus x0 x1 (proof)
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Param ccad8.. : ι → ι → ο
Param If_i^If_i : ο → ι → ι → ι
Param inv^inv : ι → (ι → ι) → ι → ι
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known a138b.. : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ccad8.. x0 x1
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known inj_linv_coddep : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . x3 ∈ x0 ⟶ inv x0 x2 (x2 x3) = x3
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem bb339.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . inj x0 x1 x2 ⟶ inj x1 x0 x3 ⟶ ccad8.. x0 x1 (proof)