Theory MMI_logic_and_sets_1

theory MMI_logic_and_sets_1
imports MMI_logic_and_sets
(* 
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.

*)


header {*\isaheader{MMI\_logic\_and\_sets\_1.thy}*}

theory MMI_logic_and_sets_1 imports MMI_logic_and_sets

begin

section{*Basic Metamath theorems, continued*}

text{*This section continues @{text "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 ∈ \<Inter> {x∈ Pow(\<real>). φ } <->
(∀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 ∈ \<Inter> {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)) --> \<Union> {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 "\<Union>{a} = a" by auto;
moreover have "a ∈ {a}" by blast;
ultimately show "\<Union> {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 ∈ \<Union> A --> (∀x. y ∈ \<Union> 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 y1 y2
assume "y1∈A ∧ ψ(y1)" and "y2∈A ∧ ψ(y2)"
with A1 have "y1∈A ∧ φ(y1)" and "y2∈A ∧ φ(y2)" by auto;
with A2 have "y1 = y2" 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 x1 x2
assume "x1∈A ∧ φ(x1)" and "x2∈A ∧ φ(x2)"
with A1 have "x1∈A ∧ ψ(x1)" and "x2∈A ∧ ψ(x2)" by auto;
with A2 have "x1 = x2" 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 = \<Union> {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 "\<Union>{a} = a" by auto;
ultimately have "a = \<Union> {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 --> \<Union>A = \<Union>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)) -->
ψ <-> \<Union> {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 "\<Union> {x ∈ A. φ(x) } = B" by auto; }
moreover
{ assume A3: "\<Union> {x ∈ A. φ(x) } = B"
moreover
from A2 obtain b where I: "{b} = {x ∈ A. φ(x) }" by auto;
moreover have "\<Union>{b} = b" by auto;
ultimately have "\<Union> {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 "ψ <-> \<Union> {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 y1 y2
assume A5: "y1 ∈ A ∧ ψ(y1)" "y2 ∈ A ∧ ψ(y2)"
with A2 have IV: "B(y1) ∈ A" and "B(y2) ∈ A" by auto;
with A4 A1 A5 have "y1 ∈ A" and "y2 ∈ A" and "B(y1) = B(y2)" by auto;
with A3 IV show "y1 = y2" by blast;
qed;

lemma MMI_reuunixfr: assumes A1: "∀ z. z ∈ C --> (∀y. z ∈ C)" and
A2: "∀ y. y ∈ A --> B(y) ∈ A" and
A3: "\<Union> {y ∈ A. ψ(y) } ∈ A --> C ∈ A" and
A4: "∀x y. x = B(y) --> φ(x) <-> ψ(y)" and
A5: "∀ y. y = \<Union> {y ∈ A. ψ(y) } --> B(y) = C" and
A6: "∀ x. x ∈ A --> (∃!y. y∈A ∧ x = B(y))"
shows "(∃!x. x∈A ∧ φ(x)) --> \<Union> {x ∈ A. φ(x) } = C"
proof;
let ?D = "\<Union> {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 "\<Union> {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 y1 y2
assume A4: "y1 ∈ C ∧ x = A(y1)" "y2 ∈ C ∧ x = A(y2)"
with A3 have "x ∈ C ∧ y1 ∈ C" and "x ∈ C ∧ y2 ∈ C" by auto;
with A2 have "x = A(y1) <-> y1 = B(x)" and "x = A(y2) <-> y2 = B(x)"
by auto;
with A4 show "y1 = y2" 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 "φ --> \<Union> A = \<Union> 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 "\<Union> A = \<Union> 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;