Theory MMI_logic_and_sets_1 (Isabelle2019: June 2019)

(* 
    This file is a part of MMIsar - a translation of Metamath's set.mm to Isabelle 2005 (ZF logic).

    Copyright (C) 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹More on logic and sets in Metamatah›

theory MMI_logic_and_sets_1 imports MMI_logic_and_sets

begin

subsection‹Basic Metamath theorems, continued›

text‹This section continues ‹MMI_logic_and_sets›. 
  It exists only so that we  don't have all Metamath basic 
  theorems in one huge file.›

(**  dependencies of nnind and peano2nn *************)

lemma MMI_pm3_27d: assumes A1: "φ ⟶ ψ ∧ ch"   
   shows "φ ⟶ ch"
   using assms by auto

(*lemma MMI_elrab: original
  assumes A1: "x = A ⟶  φ ⟷ ψ"   
   shows "A ∈ {x ∈ B. φ } ⟷ A ∈ B ∧ ψ"
   using assms by auto*)

lemma MMI_elrab:
  assumes A1: "∀x. x = A ⟶  φ(x) ⟷ ψ(x)"   
  shows "A ∈ {x ∈ B. φ(x) } ⟷ A ∈ B ∧ ψ(A)"
  using assms by auto

lemma MMI_ssrab2: 
   shows "{x ∈ A. φ(x) } ⊆ A"
  by auto

lemma MMI_anim12d: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "φ ⟶  θ ⟶ τ"   
   shows "φ ⟶ ψ ∧ θ ⟶ ch ∧ τ"
   using assms by auto

lemma MMI_mpcom: assumes A1: "ψ ⟶ φ" and
    A2: "φ ⟶ ψ ⟶ ch"   
   shows "ψ ⟶ ch"
   using assms by auto

lemma MMI_rabex: assumes A1: "A = A"   
   shows "{x ∈ A. φ(x) } = {x ∈ A. φ(x) }"
   using assms by auto

lemma MMI_rcla4cv: assumes A1: "∀x. x = A ⟶ φ(x) ⟷ ψ(x)"   
   shows "(∀x∈B. φ(x)) ⟶  A ∈ B ⟶ ψ(A)"
  using assms by auto

lemma MMI_a2i: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "(φ ⟶ ψ) ⟶ φ ⟶ ch"
   using assms by auto

lemma MMI_19_20i: assumes A1: "∀x. φ(x) ⟶ ψ(x)"   
   shows "(∀x. φ(x)) ⟶ (∀x. ψ(x))"
   using assms by auto

(*lemma MMI_elintab: assumes A1: "A = A"
   shows "A ∈ ⋂ {x∈ Pow(ℝ). φ } ⟷ 
   (∀x. φ ⟶ A ∈ x)"
   using assms by auto; original *)
(* the Additional assumption is required bc. in Isabelle
  intersection of empty set is (pretty much) undefined *)

lemma MMI_elintab: assumes A1: "A = A"
  and Additional: "{x∈B. φ(x) } ≠ 0"
   shows "A ∈ ⋂ {x∈B. φ(x) } ⟷ (∀x∈B. φ(x) ⟶ A ∈ x)"
   using assms by auto

(********* nn1suc **********)

(*lemma MMI_dfsbcq: 
   shows "A = B ⟶ 
   [ A / x ] φ ⟷ [ B / x ] φ"
  by auto

lemma MMI_sbequ: 
   shows "x = y ⟶ 
   [ x / z ] φ ⟷ [ y / z ] φ"
  by auto*)

lemma MMI_elex: 
   shows "A ∈ B ⟶ ( ∃x. x = A)"
  by auto

(*lemma MMI_hbsbc1: assumes A1: "y ∈ A ⟶ (∀x. y ∈ A)"   
   shows "(A ∈ B ⟶ [ A / x ] φ) ⟶ 
   (∀x. A ∈ B ⟶ [ A / x ] φ)"
   using assms by auto*)

(*lemma MMI_hbbi: assumes A1: "φ ⟶ (∀x. φ)" and
    A2: "ψ ⟶ (∀x. ψ)"   
   shows "φ ⟷ ψ ⟶  (∀x. φ ⟷ ψ)"
   using assms by auto;

lemma MMI_sbceq1a: 
   shows "x = A ⟶ 
   φ ⟷ [ A / x ] φ"
  by auto

lemma MMI_19_23ai: assumes A1: "ψ ⟶ (∀x. ψ)" and
    A2: "φ ⟶ ψ"   
   shows "( ∃x. φ) ⟶ ψ"
   using assms by auto*)

lemma MMI_pm5_74rd: assumes A1: "φ ⟶ 
   (ψ ⟶ ch) ⟷ 
   (ψ ⟶ θ)"   
   shows "φ ⟶ 
   ψ ⟶ 
   ch ⟷ θ"
   using assms by auto

lemma MMI_pm5_74d: assumes A1: "φ ⟶ 
   ψ ⟶ 
   ch ⟷ θ"   
   shows "φ ⟶ 
   (ψ ⟶ ch) ⟷ 
   (ψ ⟶ θ)"
   using assms by auto

(*lemma MMI_sb19_21: assumes A1: "φ ⟶ (∀x. φ)"   
   shows "[ y / x ] (φ ⟶ ψ) ⟷ 
   (φ ⟶ [ y / x ] ψ)"
   using assms by auto*)

lemma MMI_isseti: assumes A1: "A = A"   
   shows " ∃x. x = A"
   using assms by auto

(*lemma MMI_hbsbc1v: assumes A1: "A = A"   
   shows "[ A / x ] φ ⟶ (∀x. [ A / x ] φ)"
   using assms by auto

lemma MMI_sbc19_21g: assumes A1: "φ ⟶ (∀x. φ)"   
   shows "A ∈ B ⟶ 
   [ A / x ] (φ ⟶ ψ) ⟷ 
   (φ ⟶ [ A / x ] ψ)"
   using assms by auto*)

(******* nnaddclt ***********)

lemma MMI_a2d: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ"   
   shows "φ ⟶ 
   (ψ ⟶ ch) ⟶ 
   ψ ⟶ θ"
   using assms by auto

(*** nnmulclt ***)

lemma MMI_exp4b: assumes A1: "φ ∧ ψ ⟶ 
   ch ∧ θ ⟶ τ"   
   shows "φ ⟶ 
   ψ ⟶ 
   ch ⟶ 
   θ ⟶ τ"
   using assms by auto

lemma MMI_pm2_43b: assumes A1: "ψ ⟶ 
   φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ ψ ⟶ ch"
   using assms by auto

(********* nn2get nnge1t nngt1ne1t *********)
lemma MMI_biantrud: assumes A1: "φ ⟶ ψ"   
   shows "φ ⟶ 
   ch ⟷ ch ∧ ψ"
   using assms by auto

lemma MMI_anc2li: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ 
   ψ ⟶ φ ∧ ch"
   using assms by auto

lemma MMI_biantrurd: assumes A1: "φ ⟶ ψ"   
   shows "φ ⟶ 
   ch ⟷ ψ ∧ ch"
   using assms by auto

(*****nnle1eq1t-lt1nnn***********)
lemma MMI_sylc: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "θ ⟶ φ" and
    A3: "θ ⟶ ψ"   
   shows "θ ⟶ ch"
   using assms by auto

lemma MMI_con3i: assumes Aa: "φ ⟶ ψ"   
   shows "¬ψ ⟶ ¬φ"
   using assms by auto

(*********** nnleltp1t - nnaddm1clt ***********)
lemma MMI_mpan2i: assumes A1: "ch" and
    A2: "φ ⟶ 
   ψ ∧ ch ⟶ θ"   
   shows "φ ⟶ 
   ψ ⟶ θ"
   using assms by auto

lemma MMI_ralbidv: assumes A1: "∀x. φ ⟶  ψ(x) ⟷ ch(x)"   
   shows "φ ⟶ (∀x∈A. ψ(x)) ⟷ (∀x∈A. ch(x))"
   using assms by auto

lemma MMI_mp3an23: assumes A1: "ψ" and
    A2: "ch" and
    A3: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ⟶ θ"
   using assms by auto

lemma (in MMIsar0) MMI_syl5eqbrr: assumes A1: "φ ⟶ A \<ls> B" and
    A2: "A = C"   
   shows "φ ⟶ C \<ls> B"
   using assms by auto

lemma MMI_rcla4va: assumes A1: "∀x. x = A ⟶ φ(x) ⟷ ψ(A)"   
   shows "A ∈ B ∧ (∀x∈B. φ(x)) ⟶ ψ(A)"
   using assms by auto

lemma MMI_3anrot: 
   shows "φ ∧ ψ ∧ ch ⟷ ψ ∧ ch ∧ φ"
  by auto

lemma MMI_3simpc: 
   shows "φ ∧ ψ ∧ ch ⟶ ψ ∧ ch"
  by auto

lemma MMI_anandir: 
   shows "(φ ∧ ψ) ∧ ch ⟷ 
   (φ ∧ ch) ∧ ψ ∧ ch"
  by auto

lemma MMI_eqeqan12d: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ C = D"   
   shows "φ ∧ ψ ⟶ 
   A = C ⟷ B = D"
   using assms by auto

lemma MMI_3imtr3d: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "φ ⟶ 
   ψ ⟷ θ" and
    A3: "φ ⟶ 
   ch ⟷ τ"   
   shows "φ ⟶ 
   θ ⟶ τ"
   using assms by auto

lemma MMI_exp31: assumes A1: "(φ ∧ ψ) ∧ ch ⟶ θ"   
   shows "φ ⟶ 
   ψ ⟶ ch ⟶ θ"
   using assms by auto

lemma MMI_com3l: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ"   
   shows "ψ ⟶ 
   ch ⟶ 
   φ ⟶ θ"
   using assms by auto

(** original
lemma MMI_r19_21adv: assumes A1: "φ ⟶ 
   ψ ⟶ x ∈ A ⟶ ch"   
   shows "φ ⟶ 
   ψ ⟶ (∀x∈A. ch)"
   using assms by auto *)
lemma MMI_r19_21adv: assumes A1: "φ ⟶ 
   ψ ⟶ (∀x. x ∈ A ⟶ ch)"   
   shows "φ ⟶ ψ ⟶ (∀x∈A. ch)"
   using assms by auto

lemma MMI_cbvralv: assumes A1: "∀x y. x = y ⟶  φ(x) ⟷ ψ(y)"   
   shows "(∀x∈A. φ(x)) ⟷ (∀y∈A. ψ(y))"
   using assms by auto

lemma MMI_syl5ib: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "θ ⟷ ψ"   
   shows "φ ⟶ θ ⟶ ch"
   using assms by auto

lemma MMI_pm2_21i: assumes A1: "¬φ"   
   shows "φ ⟶ ψ"
   using assms by auto

lemma MMI_imim2d: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ 
   (θ ⟶ ψ) ⟶ θ ⟶ ch"
   using assms by auto

lemma MMI_syl6eqelr: assumes A1: "φ ⟶ B = A" and
    A2: "B ∈ C"   
   shows "φ ⟶ A ∈ C"
   using assms by auto

(********** nndivt,nndivtrt ****************)

lemma MMI_r19_23adv: 
  assumes A1: "∀x. φ ⟶  x ∈ A ⟶ ψ(x) ⟶ ch"   
  shows "φ ⟶ ( ∃x∈A. ψ(x)) ⟶ ch"
  using assms by auto

(*****9re - 2nn *********************)

lemma (in MMIsar0) MMI_breqtrr: assumes A1: "A \<ls> B" and
    A2: "C = B"   
   shows "A \<ls> C"
   using assms by auto

(******* ltdiv23i- lble ****************)

lemma (in MMIsar0) MMI_eqbrtr: assumes A1: "A = B" and
    A2: "B \<ls> C"   
   shows "A \<ls> C"
   using assms by auto

lemma MMI_nrex: assumes A1: "∀x. x ∈ A ⟶ ¬ψ(x)"   
   shows "¬( ∃x∈A. ψ(x))"
   using assms by auto

lemma MMI_iman: 
   shows "(φ ⟶ ψ) ⟷ 
   ¬(φ ∧ ¬ψ)"
  by auto

lemma MMI_im2anan9r: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "θ ⟶ 
   τ ⟶ η"   
   shows "θ ∧ φ ⟶ 
   ψ ∧ τ ⟶ ch ∧ η"
   using assms by auto

lemma MMI_ssel: 
   shows "A ⊆B ⟶ 
   C ∈ A ⟶ C ∈ B"
  by auto

lemma MMI_com3r: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ"   
   shows "ch ⟶ 
   φ ⟶ 
   ψ ⟶ θ"
   using assms by auto


(*lemma MMI_r19_21aivv: 
  assumes A1: "∀x y. φ ⟶  (x ∈ A ∧ y ∈ B ⟶ ψ(x,y))"   
   shows "φ ⟶ (∀x∈A. ∀y∈B. ψ(x,y))"
   using assms by auto;*)


lemma MMI_r19_21aivv: 
  assumes A1: "φ ⟶  (∀x y.  x ∈ A ∧ y ∈ B ⟶ ψ(x,y))"   
   shows "φ ⟶ (∀x∈A. ∀y∈B. ψ(x,y))"
   using assms by auto

lemma MMI_reucl2: 
   shows 
  "(∃!x. x∈A ∧ φ(x)) ⟶ ⋃ {x ∈ A. φ(x)} ∈ {x ∈ A. φ(x) }"
proof
  assume "∃!x. x∈A ∧ φ(x)"
  then obtain a where I: "{a} = {x∈A. φ(x)}" by auto
  moreover have "⋃{a} = a" by auto
  moreover have "a ∈ {a}" by blast
  ultimately show "⋃ {x ∈ A. φ(x)} ∈ {x ∈ A. φ(x) }"
    by simp
qed

lemma MMI_hbra1: 
   shows "(∀x∈A. φ(x)) ⟶ (∀x. ∀x∈A. φ(x))"
  by auto

lemma MMI_hbrab: assumes A1: "φ ⟶ (∀x. φ)" and
    A2: "z ∈ A ⟶ (∀x. z ∈ A)"   
   shows "z ∈ {y ∈ A. φ } ⟶ 
   (∀x. z ∈ {y ∈ A. φ })"
   using assms by auto

lemma MMI_hbuni: assumes A1: "y ∈ A ⟶ (∀x. y ∈ A)"   
   shows "y ∈ ⋃ A ⟶  (∀x. y ∈ ⋃ A)"
   using assms by auto

lemma (in MMIsar0) MMI_hbbr: assumes A1: "y ∈ A ⟶ (∀x. y ∈ A)" and
    A2: "y ∈ R ⟶ (∀x. y ∈ R)" and
    A3: "y ∈ B ⟶ (∀x. y ∈ B)"   
   shows 
  "A \<lsq> B ⟶ (∀x. A \<lsq> B)"
  "A \<ls> B ⟶ (∀x. A \<ls> B)"
   using assms by auto

lemma MMI_rcla4: assumes A1: "ψ ⟶ (∀x. ψ)" and
    A2: "∀x. x = A ⟶ φ ⟷ ψ"   
   shows "A ∈ B ⟶  (∀x∈B. φ) ⟶ ψ"
   using assms by auto

lemma twimp2eq: assumes "p⟶q" and "q⟶p" shows "p⟷q"
  using assms by blast

lemma MMI_cbvreuv: assumes A1: "∀x y. x = y ⟶  φ(x) ⟷ ψ(y)"   
   shows "(∃!x. x∈A∧φ(x)) ⟷ (∃!y. y∈A∧ψ(y))"
   using assms
proof -
  { assume A2: "∃!x. x∈A ∧ φ(x)"
    then obtain a where I: "a∈A" and II: "φ(a)" by auto
    with A1 have "ψ(a)" by simp
    with I have "∃y. y∈A∧ψ(y)" by auto
    moreover
    { fix y⇩₁ y⇩₂
      assume "y⇩₁∈A ∧ ψ(y⇩₁)" and "y⇩₂∈A ∧ ψ(y⇩₂)"
      with A1 have "y⇩₁∈A ∧ φ(y⇩₁)" and "y⇩₂∈A ∧ φ(y⇩₂)" by auto
      with A2 have "y⇩₁ = y⇩₂" by auto }
    ultimately have "∃!y. y∈A ∧ ψ(y)" by auto
  } then have "(∃!x. x∈A∧φ(x)) ⟶ (∃!y. y∈A∧ψ(y))" by simp
  moreover
  { assume A2: "∃!y. y∈A ∧ ψ(y)"
    then obtain a where I: "a∈A" and II: "ψ(a)" by auto
    with A1 have "φ(a)" by simp
    with I have "∃x. x∈A ∧ φ(x)" by auto
    moreover
    { fix x⇩₁ x⇩₂
      assume "x⇩₁∈A ∧ φ(x⇩₁)" and "x⇩₂∈A ∧ φ(x⇩₂)"
      with A1 have "x⇩₁∈A ∧ ψ(x⇩₁)" and "x⇩₂∈A ∧ ψ(x⇩₂)" by auto
      with A2 have "x⇩₁ = x⇩₂" by auto }
    ultimately have "∃!x. x∈A ∧ φ(x)" by auto
  } then have "(∃!y. y∈A∧ψ(y)) ⟶ (∃!x. x∈A∧φ(x))" by simp
  ultimately show ?thesis by (rule twimp2eq)
qed
      
lemma MMI_hbeleq: assumes A1: "y ∈ A ⟶ (∀x. y ∈ A)"   
   shows "y = A ⟶ (∀x. y = A)"
   using assms by auto

lemma MMI_ralbid: assumes A1: "φ ⟶ (∀x. φ)" and
    A2: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ⟶ 
   (∀x∈A. ψ) ⟷ (∀x∈A. ch)"
   using assms by auto

lemma MMI_reuuni3: 
  assumes A1: "∀x y. x = y ⟶  φ(x) ⟷ ψ(y)" and
    A2: "∀x. x = ⋃ {y ∈ A. ψ(y) } ⟶  (φ(x) ⟷ ch)"   
   shows "(∃!x. x∈A ∧ φ(x)) ⟶ ch"
proof
  assume A3: "∃!x. x∈A ∧ φ(x)"
  then obtain a where I: "{a} = {x∈A. φ(x)}" by auto
  with A1 have "{a} = {y∈A. ψ(y)}" by auto
  moreover have "⋃{a} = a" by auto
  ultimately have "a = ⋃ {y ∈ A. ψ(y) }" by auto
  with A2 have "φ(a) ⟷ ch" by simp
  moreover 
  have "a ∈ {a}" by simp
  with I have "φ(a)" by simp
  ultimately show "ch" by simp
qed

(******* lbinfm ****************)

lemma MMI_ssex: assumes A1: "B = B"   
   shows "A ⊆B ⟶ A = A"
   using assms by auto

lemma MMI_rabexg: 
   shows "A ∈ B ⟶ 
   {x ∈ A. φ(x) } = {x ∈ A. φ(x) }"
  by auto

lemma MMI_uniexg: 
   shows "A ∈ B ⟶ ⋃A = ⋃A "
  by auto

(*lemma (in MMIsar0) MMI_brcnvg: 
  shows "A ∈ C ∧ B ∈ D ⟶  A > B ⟷ B \<ls> A"
  using cltrr_def convcltrr_def converse_iff by auto original *)

lemma (in MMIsar0) MMI_brcnvg: 
  shows "A = A ∧ B = B ⟶  A > B ⟷ B \<ls> A"
  using cltrr_def convcltrr_def converse_iff by auto

lemma MMI_r19_21aiva: assumes A1: "∀x. φ ∧ x ∈ A ⟶ ψ(x)"   
   shows "φ ⟶ (∀x∈A. ψ(x))"
   using assms by auto

lemma MMI_ancrd: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ 
   ψ ⟶ ch ∧ ψ"
   using assms by auto

lemma MMI_reuuni2: 
  assumes A1: "∀x. x = B ⟶ φ(x) ⟷ ψ"   
   shows "B ∈ A ∧ (∃!x. x∈A∧φ(x)) ⟶ 
   ψ ⟷  ⋃ {x ∈ A. φ(x) } = B"
proof
  assume A2: "B ∈ A ∧ (∃!x. x∈A∧φ(x))"
  { assume "ψ"
    with A1 have "φ(B)" by simp
    with A2 have "{x ∈ A. φ(x) } = {B}" by auto
    then have "⋃ {x ∈ A. φ(x) } = B" by auto }
  moreover
  { assume A3: "⋃ {x ∈ A. φ(x) } = B"
    moreover 
    from A2 obtain b where I: "{b} = {x ∈ A. φ(x) }" by auto
    moreover have "⋃{b} = b" by auto
    ultimately have "⋃ {x ∈ A. φ(x) } = b" by simp
    with A3 I have "{B} = {x ∈ A. φ(x) }" by simp
    moreover have "B ∈ {B}" by simp
    ultimately have "φ(B)" by auto
    with A1 have "ψ" by simp }
  ultimately show "ψ ⟷  ⋃ {x ∈ A. φ(x) } = B" by blast
qed

lemma (in MMIsar0) MMI_cnvso: 
   shows "\<cltrrset> Orders A ⟷ converse(\<cltrrset>) Orders A"
  using cnvso by simp

lemma (in MMIsar0) MMI_supeu: assumes A1: "\<cltrrset> Orders A"   
   shows "( ∃x∈A. (∀y∈B. ¬(x\<ls>y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))) ⟶ 
   (∃!x. x∈A∧(∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z)))"
proof
  assume 
    "∃x∈A. (∀y∈B. ¬(x\<ls>y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"
  then obtain x where 
    "x∈A"  "∀y∈B. ⟨x,y⟩ ∉ \<cltrrset>"  
    "∀y∈A. ⟨y,x⟩ ∈ \<cltrrset>  ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ \<cltrrset>)"
    using cltrr_def by auto
  with A1 have
    "∃!x. x∈A∧(∀y∈B. ⟨x,y⟩ ∉ \<cltrrset>) ∧ (∀y∈A. ⟨y,x⟩ ∈ \<cltrrset> ⟶ 
    ( ∃z∈B. ⟨y,z⟩ ∈ \<cltrrset>))"
    using supeu by simp
  then show
    "∃!x. x∈A∧(∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"
    using cltrr_def by simp
qed

(** This is actually not in Metamath, we need it only because 
    Isabelle does not support $a R b$ notation for relations $R$. 
    Metamath covers both we MMI_supeu and MMI_infeu 
    in one theorem, we need two **)

lemma (in MMIsar0) MMI_infeu: assumes A1: "converse(\<cltrrset>) Orders A"   
   shows 
  "(∃x∈A. (∀y∈B. ¬(x > y)) ∧ (∀y∈A. y  >  x ⟶ ( ∃z∈B. y  >  z))) ⟶ 
   (∃!x. x∈A∧(∀y∈B. ¬(x  >  y)) ∧ (∀y∈A. y  >  x ⟶ ( ∃z∈B. y  >  z)))"
proof
  let ?r = "converse(\<cltrrset>)"
  assume 
    "∃x∈A. (∀y∈B. ¬(x > y)) ∧ (∀y∈A. y  >  x ⟶ ( ∃z∈B. y  >  z))"
  then obtain x where 
    "x∈A"  "∀y∈B. ⟨x,y⟩ ∉ ?r"  
    "∀y∈A. ⟨y,x⟩ ∈ ?r  ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?r)"
    using convcltrr_def by auto
  with A1 have
    "∃!x. x∈A∧(∀y∈B. ⟨x,y⟩ ∉ ?r) ∧ (∀y∈A. ⟨y,x⟩ ∈ ?r ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?r))"
    by (rule supeu)
  then show
    "∃!x. x∈A∧(∀y∈B. ¬(x  >  y)) ∧ (∀y∈A. y  >  x ⟶ ( ∃z∈B. y  >  z))"
    using convcltrr_def by simp
qed

(******** lbinfmcl, lbinfmle ***********************)

lemma MMI_eqeltrd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ B ∈ C"   
   shows "φ ⟶ A ∈ C"
   using assms by auto

lemma (in MMIsar0) MMI_eqbrtrd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ B \<lsq> C"   
   shows "φ ⟶ A \<lsq> C"
   using assms by auto

(****** sup2 ************************************)

lemma MMI_df_ral: shows "(∀x∈A. φ(x)) ⟷ (∀x. x∈A ⟶ φ(x))"
  by auto

lemma MMI_df_3an: shows  "(φ ∧ ψ  ∧ ch ) ⟷ ( (φ ∧ ψ ) ∧ ch )"
  by auto

lemma MMI_pm2_43d: assumes A1: "φ ⟶ 
   ψ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ ψ ⟶ ch"
   using assms by auto

lemma MMI_biimprcd: assumes A1: "φ ⟶ 
   ψ ⟷ ch"   
   shows "ch ⟶ 
   φ ⟶ ψ"
   using assms by auto

lemma MMI_19_20dv: assumes A1: "∀ y. φ ⟶ ψ(y) ⟶ ch(y)"   
   shows "φ ⟶  (∀y. ψ(y)) ⟶ (∀y. ch(y))"
   using assms by auto

lemma MMI_cla4ev: assumes A1: "A = A" and
    A2: "∀x. x = A ⟶  φ(x) ⟷ ψ(x)"   
   shows "ψ(A) ⟶ ( ∃x. φ(x))"
   using assms by auto

lemma MMI_19_23adv: assumes A1: "∀x. φ ⟶ ψ(x) ⟶ ch"   
   shows "φ ⟶  ( ∃x. ψ(x)) ⟶ ch"
   using assms by auto

lemma MMI_cbvexv: assumes A1: "∀x y. x = y ⟶ φ(x) ⟷ ψ(y)"   
   shows "( ∃x. φ(x)) ⟷ ( ∃y. ψ(y))"
   using assms by auto

(********** sup3 *********************)

lemma MMI_bicomi: assumes A1: "φ ⟷ ψ"   
   shows "ψ ⟷ φ"
   using assms by auto

lemma MMI_syl9: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "θ ⟶ ch ⟶ τ"   
   shows "φ ⟶ 
   θ ⟶ 
   ψ ⟶ τ"
   using assms by auto

lemma MMI_imp31: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ"   
   shows "(φ ∧ ψ) ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_pm5_32i: assumes A1: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ∧ ψ ⟷ φ ∧ ch"
   using assms by auto

(****** infm3 *************************)

lemma MMI_3impib: assumes A1: "φ ⟶ 
   ψ ∧ ch ⟶ θ"   
   shows "φ ∧ ψ ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_pm4_71rd: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ 
   ψ ⟷ ch ∧ ψ"
   using assms by auto

lemma MMI_exbidv: assumes A1: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ⟶ 
   ( ∃x. ψ) ⟷ ( ∃x. ch)"
   using assms by auto

(** original
lemma MMI_rexxfr: assumes A1: "y ∈ B ⟶ A ∈ B" and
    A2: "x ∈ B ⟶ ( ∃y∈B. x = A)" and
    A3: "x = A ⟶ 
   φ ⟷ ψ"   
   shows "( ∃x∈B. φ) ⟷ ( ∃y∈B. ψ)"
   using assms by auto *********)

lemma MMI_rexxfr: assumes A1: "∀y. y ∈ B ⟶ A(y) ∈ B" and
    A2: "∀ x. x ∈ B ⟶ ( ∃y∈B. x = A(y))" and
    A3: "∀ x y. x = A(y) ⟶ ( φ(x) ⟷ ψ(y) ) "   
   shows "( ∃x∈B. φ(x)) ⟷ ( ∃y∈B. ψ(y))"
proof
  assume "∃x∈B. φ(x)"
  then obtain x where "x∈B" and I: "φ(x)" by auto
  with A2 obtain y where II: "y∈B" and "x=A(y)" by auto
  with A3 I have "ψ(y)" by simp
  with II show "∃y∈B. ψ(y)" by auto
next assume "∃y∈B. ψ(y)"
  then obtain y where "y∈B" and III: "ψ(y)" by auto
  with A1 have IV: "A(y) ∈ B" by simp
  with A2 obtain x where "x∈B" and "A(x) = A(y)" by auto
  with A3 III have "φ(A(y))" by auto
  with IV show "∃x∈B. φ(x)" by auto
qed
  
lemma MMI_n0: 
   shows "¬(A = 0) ⟷ ( ∃x. x ∈ A)"
  by auto

lemma MMI_rabn0: 
   shows "¬({x ∈ A. φ(x) } = 0) ⟷ ( ∃x∈A. φ(x))"
  by auto

lemma MMI_impexp: 
   shows "(φ ∧ ψ ⟶ ch) ⟷ 
   (φ ⟶ ψ ⟶ ch)"
  by auto

lemma MMI_albidv: assumes A1: "∀x. φ ⟶  ψ(x) ⟷ ch(x)"   
   shows "φ ⟶  (∀x. ψ(x)) ⟷ (∀x. ch(x))"
   using assms by auto

lemma MMI_ralxfr: assumes A1: "∀y. y ∈ B ⟶ A(y) ∈ B" and
    A2: "∀x. x ∈ B ⟶ ( ∃y∈B. x = A(y))" and
    A3: "∀x y. x = A(y) ⟶  φ(x) ⟷ ψ(y)"   
   shows "(∀x∈B. φ(x)) ⟷ (∀y∈B. ψ(y))"
proof
  assume A4: "∀x∈B. φ(x)"
  { fix y assume "y∈B"
    with A1 A3 A4 have "ψ(y)" by auto
  } then show "∀y∈B. ψ(y)" by simp
next assume A5: "∀y∈B. ψ(y)"
  { fix x assume "x∈B"
    with A2 A3 A5 have "φ(x)" by auto
  } then show "∀x∈B. φ(x)" by simp
qed

lemma MMI_rexbidv: assumes A1: "∀x. φ ⟶  ψ(x) ⟷ ch(x)"   
   shows "φ ⟶ ( ∃x∈A. ψ(x)) ⟷ ( ∃x∈A. ch(x))"
   using assms by auto

lemma MMI_imbi1i: assumes Aa: "φ ⟷ ψ"   
   shows "(φ ⟶ ch) ⟷ (ψ ⟶ ch)"
   using assms by auto

lemma MMI_3bitr4r: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ φ" and
    A3: "θ ⟷ ψ"   
   shows "θ ⟷ ch"
   using assms by auto

lemma MMI_rexbiia: assumes A1: "∀x. x ∈ A ⟶  φ(x) ⟷ ψ(x)"   
   shows "( ∃x∈A. φ(x)) ⟷ ( ∃x∈A. ψ(x))"
   using assms by auto

lemma MMI_anass: 
   shows "(φ ∧ ψ) ∧ ch ⟷ φ ∧ ψ ∧ ch"
  by auto

lemma MMI_rexbii2: assumes A1: "∀x. x ∈ A ∧ φ(x) ⟷ x ∈ B ∧ ψ(x)"   
   shows "( ∃x∈A. φ(x)) ⟷ ( ∃x∈B. ψ(x))"
   using assms by auto

lemma MMI_sylibrd: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "φ ⟶ 
   θ ⟷ ch"   
   shows "φ ⟶ 
   ψ ⟶ θ"
   using assms by auto

(************** suprcl, suprub *******************)

lemma (in MMIsar0) MMI_supcl: assumes A1:   "\<cltrrset> Orders A"
  shows 
  "( ∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ 
  ( ∃z∈B. y \<ls> z))) ⟶  Sup(B,A,\<cltrrset>) ∈ A"
proof
  let ?R = "\<cltrrset>"
  assume 
    "∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"
  then have 
    "∃x∈A. (∀y∈B. ¬(⟨x,y⟩ ∈ ?R) ) ∧ (∀y∈A. ⟨y,x⟩ ∈ ?R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?R))"
    using cltrr_def by simp
  with A1 show "Sup(B,A,?R) ∈ A" by (rule sup_props)
qed

lemma (in MMIsar0) MMI_supub: assumes A1: "\<cltrrset> Orders A"   
   shows 
  "( ∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))) ⟶ 
   C ∈ B ⟶ ¬( Sup(B,A,\<cltrrset>) \<ls> C)"
proof
  let ?R = "\<cltrrset>"
  assume 
    "∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"
  then have
    "∃x∈A. (∀y∈B. ⟨x,y⟩ ∉ ?R) ∧ (∀y∈A. ⟨y,x⟩ ∈ ?R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?R))"
    using cltrr_def by simp
  with A1 have I: "∀y∈B. ⟨Sup(B,A,?R),y⟩ ∉ ?R" by (rule sup_props)
  { assume "C ∈ B"
    with I have  "¬( Sup(B,A,?R) \<ls> C)" using cltrr_def by simp
  } then show "C ∈ B ⟶ ¬( Sup(B,A,?R) \<ls> C)" by simp
qed

lemma MMI_sseld: assumes A1: "φ ⟶ A ⊆ B"   
   shows "φ ⟶ C ∈ A ⟶ C ∈ B"
   using assms by auto

(********suprlub - suprleub **********************)

lemma (in MMIsar0) MMI_suplub: assumes A1: "\<cltrrset> Orders A"   
   shows "( ∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ 
  (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))) ⟶ 
   C ∈ A ∧ C \<ls> Sup(B,A,\<cltrrset>) ⟶ ( ∃z∈B. C \<ls> z)"
proof
  let ?R = "\<cltrrset>"
  assume 
    "∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"
  then have
    "∃x∈A. (∀y∈B. ⟨x,y⟩ ∉ ?R) ∧ (∀y∈A. ⟨y,x⟩ ∈ ?R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?R))"
    using cltrr_def by simp
  with A1 have I:
    "∀y∈A. ⟨y,Sup(B,A,?R)⟩ ∈ ?R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?R )"
    by (rule sup_props)
  then show "C ∈ A ∧ C \<ls> Sup(B,A,?R) ⟶ ( ∃z∈B. C \<ls> z)"
    using cltrr_def by simp
qed

lemma (in MMIsar0) MMI_supnub: assumes A1: "\<cltrrset> Orders A"   
   shows 
  "(∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ 
  ( ∃z∈B. y \<ls> z))) ⟶ 
   C ∈ A ∧ (∀z∈B. ¬(C \<ls> z)) ⟶ ¬(C \<ls> Sup(B,A,\<cltrrset>))"
proof
  let ?R = "\<cltrrset>"
  assume 
    "∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"
  then have
    "∃x∈A. (∀y∈B. ⟨x,y⟩ ∉ ?R) ∧ (∀y∈A. ⟨y,x⟩ ∈ ?R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ ?R))"
    using cltrr_def by simp
  with A1 show
    "C ∈ A ∧ (∀z∈B. ¬(C \<ls> z)) ⟶ ¬(C \<ls> Sup(B,A,\<cltrrset>))"
    using cltrr_def supnub by simp
qed

lemma MMI_pm5_32d: assumes A1: "φ ⟶ ψ ⟶  ch ⟷ θ"   
   shows "φ ⟶  ψ ∧ ch ⟷ ψ ∧ θ"
   using assms by auto

(********* sup3i - suprnubi **********************)

lemma (in MMIsar0) MMI_supcli: 
  assumes A1: "\<cltrrset> Orders A" and A2: 
  "∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"   
  shows "Sup(B,A,\<cltrrset>) ∈ A"
  using assms MMI_supcl by simp

lemma (in MMIsar0) MMI_suplubi: assumes A1: "\<cltrrset> Orders A" and
  A2: "∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"  
  shows "C ∈ A ∧ C \<ls> Sup(B,A,\<cltrrset>) ⟶ ( ∃z∈B. C \<ls> z)"
proof -
  from A1 have "( ∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ 
    (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))) ⟶ 
    C ∈ A ∧ C \<ls> Sup(B,A,\<cltrrset>) ⟶ ( ∃z∈B. C \<ls> z)"
    by (rule MMI_suplub)
  with A2 show "C ∈ A ∧ C \<ls> Sup(B,A,\<cltrrset>) ⟶ ( ∃z∈B. C \<ls> z)"
    by simp
qed

lemma  (in MMIsar0) MMI_supnubi: assumes A1: "\<cltrrset> Orders A" and
    A2: " ∃x∈A. (∀y∈B. ¬(x \<ls> y)) ∧ 
  (∀y∈A. y \<ls> x ⟶ ( ∃z∈B. y \<ls> z))"   
   shows "C ∈ A ∧ (∀z∈B. ¬(C \<ls> z)) ⟶ ¬(C \<ls>Sup(B,A,\<cltrrset>))"
   using assms  MMI_supnub by simp

(************ suprleubi - dfinfmr *********************)

lemma MMI_reuunixfr_helper: assumes
  A1: "∀x y. x = B(y) ⟶ φ(x) ⟷ ψ(y)" and 
  A2: "∀y. y∈A ⟶ B(y) ∈ A" and
  A3: "∀ x. x ∈ A ⟶  (∃!y. y∈A ∧ x = B(y))" and
  A4: "∃!x. x∈A ∧ φ(x)"
shows "∃!y. y∈A ∧ ψ(y)"
proof
  from A4 obtain x where I: "x∈A" and II: "φ(x)" by auto
  with A3 obtain y where III: "y∈A" and "x = B(y)" by auto
  with A1 II show "∃y. y ∈ A ∧ ψ(y)" by auto
next fix y⇩₁ y⇩₂
  assume A5: "y⇩₁ ∈ A ∧ ψ(y⇩₁)"   "y⇩₂ ∈ A ∧ ψ(y⇩₂)"
  with A2 have IV: "B(y⇩₁) ∈ A" and "B(y⇩₂) ∈ A" by auto
  with A4 A1 A5 have "y⇩₁ ∈ A" and "y⇩₂ ∈ A" and "B(y⇩₁) = B(y⇩₂)" by auto
  with A3 IV show "y⇩₁ = y⇩₂" by blast
qed
 
lemma MMI_reuunixfr: assumes A1: "∀ z. z ∈ C ⟶ (∀y. z ∈ C)" and
    A2: "∀ y. y ∈ A ⟶ B(y) ∈ A" and
    A3: "⋃ {y ∈ A. ψ(y) } ∈ A ⟶ C ∈ A" and
    A4: "∀x y. x = B(y) ⟶  φ(x) ⟷ ψ(y)" and
    A5: "∀ y. y = ⋃ {y ∈ A. ψ(y) } ⟶ B(y) = C" and
    A6: "∀ x. x ∈ A ⟶  (∃!y. y∈A ∧ x = B(y))"   
   shows "(∃!x. x∈A ∧ φ(x)) ⟶  ⋃ {x ∈ A. φ(x) } = C"
proof
  let ?D = "⋃ {y ∈ A. ψ(y)}"
  assume A7: "∃!x. x∈A ∧ φ(x)"
  with A4 A2 A6 have I: "∃!y. y∈A ∧ ψ(y)" by (rule MMI_reuunixfr_helper)
  with A3 have T: "C ∈ A" using ZF1_1_L9 by simp 
  from A4 A5 have "φ(C) ⟷ ψ(?D)" by auto
  moreover from I have "ψ(?D)" by (rule ZF1_1_L9)
  ultimately have "φ(C)" by simp
  with T A7 show "⋃ {x ∈ A. φ(x) } = C" by auto
qed
  
lemma MMI_hbrab1: 
   shows "y ∈ {x ∈ A. φ(x) } ⟶  (∀x. y ∈ {x ∈ A. φ(x) })"
  by auto

lemma MMI_reuhyp: assumes A1: "∀x. x ∈ C ⟶ B(x) ∈ C" and
    A2: "∀ x y.  x ∈ C ∧ y ∈ C ⟶  x = A(y) ⟷ y = B(x)"   
   shows "∀ x. x ∈ C ⟶ (∃!y. y∈C ∧ x = A(y))"
proof -
  { fix x
    assume A3: "x∈C"
    with A1 have I: "B(x) ∈ C" by simp
    with A2 A3 have II: "x = A(B(x))" by simp
    have "∃!y. y∈C ∧ x = A(y)"
    proof
      from I II show "∃y. y∈C ∧ x = A(y)" by auto
    next fix y⇩₁ y⇩₂ 
      assume A4: "y⇩₁ ∈ C ∧ x = A(y⇩₁)"   "y⇩₂ ∈ C ∧ x = A(y⇩₂)"
      with A3 have "x ∈ C ∧ y⇩₁ ∈ C" and "x ∈ C ∧ y⇩₂ ∈ C" by auto
      with A2 have "x = A(y⇩₁) ⟷ y⇩₁ = B(x)" and "x = A(y⇩₂) ⟷ y⇩₂ = B(x)"
	by auto
      with A4 show "y⇩₁ = y⇩₂" by auto
    qed
  } then show ?thesis by simp
qed

lemma (in MMIsar0) MMI_brcnv: assumes A1: "A = A" and
    A2: "B = B"   
   shows "A > B ⟷ B \<ls> A"
   using convcltrr_def cltrr_def by auto

lemma MMI_imbi12i: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ θ"   
   shows "(φ ⟶ ch) ⟷  (ψ ⟶ θ)"
   using assms by auto

lemma MMI_ralbii: assumes A1: "∀ x. φ(x) ⟷ ψ(x)"   
   shows "(∀x∈A. φ(x)) ⟷ (∀x∈A. ψ(x))"
   using assms by auto

lemma MMI_rabbidv: assumes A1: "∀ x. φ ⟶ x ∈ A ⟶  ψ(x) ⟷ ch(x)"   
   shows "φ ⟶  {x ∈ A. ψ(x) } = {x ∈ A. ch(x) }"
   using assms by auto

lemma MMI_unieqd: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ ⋃ A = ⋃ B"
   using assms by auto

(************ infmsup, infmrcl **********************)

lemma MMI_rabbii: assumes A1: "∀ x. x ∈ A ⟶  ψ(x) ⟷ ch(x)"   
   shows "{x ∈ A. ψ(x) } = {x ∈ A. ch(x) }"
   using assms by auto

lemma MMI_unieqi: assumes A1: "A = B"   
   shows "⋃ A = ⋃ B"
   using assms by auto

lemma MMI_syl5rbb: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "θ ⟷ ψ"   
   shows "φ ⟶ 
   ch ⟷ θ"
   using assms by auto

lemma MMI_reubii: assumes A1: "∀x. φ(x) ⟷ ψ(x)"   
   shows "(∃!x. x∈A ∧ φ(x)) ⟷ (∃!x. x∈A ∧ ψ(x))"
   using assms by auto

lemma MMI_3imtr3: assumes A1: "φ ⟶ ψ" and
    A2: "φ ⟷ ch" and
    A3: "ψ ⟷ θ"   
   shows "ch ⟶ θ"
   using assms by auto

lemma MMI_syl6d: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ" and
    A2: "φ ⟶ 
   θ ⟶ τ"   
   shows "φ ⟶ 
   ψ ⟶ ch ⟶ τ"
   using assms by auto

lemma MMI_n0i: 
   shows "B ∈ A ⟶ ¬(A = 0)"
  by auto

end