:: The Reflection Theorem
::  by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies CLASSES2, ZF_LANG, FUNCT_1, SUBSET_1, ZF_MODEL, TARSKI, ORDINAL1,
      XBOOLE_0, ZFMISC_1, CARD_1, BVFUNC_2, XBOOLEAN, ZFMODEL1, RELAT_1,
      ORDINAL2, ORDINAL4, CARD_3, CLASSES1, NUMBERS, NAT_1, ARYTM_3, XXREAL_0,
      REALSET1, FUNCT_2, ZF_REFLE, CARD_FIL, CARD_5;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, XCMPLX_0,
      NAT_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, ZF_MODEL, ZFMODEL1, ORDINAL2,
      NUMBERS, CARD_3, CLASSES1, CLASSES2, ZF_LANG, ORDINAL4, ZF_LANG1, CARD_5,
      CARD_FIL, CARD_LAR, XXREAL_0;
 constructors ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, CLASSES1, CARD_3,
      ORDINAL4, ZF_MODEL, ZFMODEL1, ZF_LANG1, RELSET_1, CARD_LAR, CARD_FIL,
      CARD_5, NUMBERS;
 registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0,
      CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, CARD_5,
      CARD_LAR, CARD_3, RELAT_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin

reserve W for Universe,
  H for ZF-formula,
  x,y,z,X for set,
  k for Variable,
  f for Function of VAR,W,
  u,v for Element of W;

theorem :: ZF_REFLE:1
  W |= the_axiom_of_pairs;

theorem :: ZF_REFLE:2
  W |= the_axiom_of_unions;

theorem :: ZF_REFLE:3
  omega in W implies W |= the_axiom_of_infinity;

theorem :: ZF_REFLE:4
  W |= the_axiom_of_power_sets;

theorem :: ZF_REFLE:5
  for H st { x.0,x.1,x.2 } misses Free H holds W |=
  the_axiom_of_substitution_for H;

theorem :: ZF_REFLE:6
  omega in W implies W is being_a_model_of_ZF;

reserve F for Function,
  A,B,C for Ordinal,
  a,b,b1,b2,c for Ordinal of W,
  fi for Ordinal-Sequence,
  phi for Ordinal-Sequence of W,
  H for ZF-formula;

scheme :: ZF_REFLE:sch 1
  ALFA9Universe { W()->Universe, D() -> non empty set, P[set,set] }: ex F st
dom F = D() & for d being Element of D() ex a being Ordinal of W() st a = F.d &
  P[d,a] & for b being Ordinal of W() st P[d,b] holds a c= b
provided
 for d being Element of D() ex a being Ordinal of W() st P[d,a];

theorem :: ZF_REFLE:7
  x is Ordinal of W iff x in On W;

reserve psi for Ordinal-Sequence;

scheme :: ZF_REFLE:sch 2
  OrdSeqOfUnivEx { W()->Universe, P[object,object] }:
 ex phi being Ordinal-Sequence
  of W() st for a being Ordinal of W() holds P[a,phi.a]
provided
 for a being Ordinal of W() ex b being Ordinal of W() st P[a,b];

scheme :: ZF_REFLE:sch 3
  UOSExist { W()->Universe, a()->Ordinal of W(), C(Ordinal,Ordinal)->Ordinal
of W(), D(Ordinal,Sequence)->Ordinal of W() } : ex phi being Ordinal-Sequence
of W() st phi.0-element_of W() = a() & (for a being Ordinal of W() holds phi.(
succ a) = C(a,phi.a)) & for a being Ordinal of W() st a <> 0-element_of W() & a
  is limit_ordinal holds phi.a = D(a,phi|a);

scheme :: ZF_REFLE:sch 4
  UniverseInd { W()->Universe, P[Ordinal] }: for a being Ordinal of W() holds
  P[a]
provided
 P[0-element_of W()] and
 for a being Ordinal of W() st P[a] holds P[succ a] and
 for a being Ordinal of W() st a <> 0-element_of W() & a is
limit_ordinal & for b being Ordinal of W() st b in a holds P[b] holds P[a];

definition
  let f be Function, W be Universe, a be Ordinal of W;
  func union(f,a) -> set equals
:: ZF_REFLE:def 1
  Union (W|`(f|Rank a));
end;

theorem :: ZF_REFLE:8
  for L being Sequence,A holds L|Rank A is Sequence;

theorem :: ZF_REFLE:9
  for L being Ordinal-Sequence,A holds L|Rank A is Ordinal-Sequence;

theorem :: ZF_REFLE:10
  Union psi is Ordinal;

theorem :: ZF_REFLE:11
  Union (X|`psi) is epsilon-transitive epsilon-connected set;

theorem :: ZF_REFLE:12
  On Rank A = A;

theorem :: ZF_REFLE:13
  psi|Rank A = psi|A;

definition
  let phi be Ordinal-Sequence, W be Universe, a be Ordinal of W;
  redefine func union(phi,a) -> Ordinal of W;
end;

theorem :: ZF_REFLE:14
  for phi being Ordinal-Sequence of W holds union(phi,a) = Union (
  phi|a) & union(phi|a,a) = Union (phi|a);

definition
  let W be Universe, a,b be Ordinal of W;
  redefine func a \/ b -> Ordinal of W;
end;

registration
  let W;
  cluster non empty for Element of W;
end;

definition
  let W;
  mode Subclass of W is non empty Subset of W;
end;

definition
  let W;
  let IT be Sequence of W;

  attr IT is DOMAIN-yielding means
:: ZF_REFLE:def 2

  dom IT = On W;
end;

registration
  let W;
  cluster DOMAIN-yielding non-empty for Sequence of W;
end;

definition
  let W;
  mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding Sequence of W;
end;

definition
  let W;
  let L be DOMAIN-Sequence of W;
  redefine func Union L -> Subclass of W;
  let a;
  redefine func L.a -> non empty Element of W;
end;

reserve L for DOMAIN-Sequence of W,
  n for Element of NAT,
  f for Function of VAR,L.a;

theorem :: ZF_REFLE:15
  a in dom L;

theorem :: ZF_REFLE:16
  L.a c= Union L;

theorem :: ZF_REFLE:17
  NAT,VAR are_equipotent;

theorem :: ZF_REFLE:18
  sup X c= succ union On X;

theorem :: ZF_REFLE:19
  X in W implies sup X in W;

reserve x1 for Variable;

::$N Reflection Theorem
theorem :: ZF_REFLE:20
  omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {}
  & a is limit_ordinal holds L.a = Union (L|a)) implies for H ex phi st phi is
increasing & phi is continuous & for a st phi.a = a & {} <> a for f holds Union
  L,(Union L)!f |= H iff L.a,f |= H;

begin :: Addenda
:: from CARD_LAR, 2010.03.11, A.T.

reserve M for non countable Aleph;

theorem :: ZF_REFLE:21
  M is strongly_inaccessible implies Rank M is being_a_model_of_ZF;