:: The Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2016 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;