:: by Grzegorz Bancerek

::

:: Received August 10, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th5: :: ZF_REFLE:5

for W being Universe

for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

W |= the_axiom_of_substitution_for H

for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

W |= the_axiom_of_substitution_for H

proof end;

scheme :: ZF_REFLE:sch 1

ALFA9Universe{ F_{1}() -> Universe, F_{2}() -> non empty set , P_{1}[ set , set ] } :

ALFA9Universe{ F

ex F being Function st

( dom F = F_{2}() & ( for d being Element of F_{2}() ex a being Ordinal of F_{1}() st

( a = F . d & P_{1}[d,a] & ( for b being Ordinal of F_{1}() st P_{1}[d,b] holds

a c= b ) ) ) )

provided
( dom F = F

( a = F . d & P

a c= b ) ) ) )

proof end;

theorem :: ZF_REFLE:7

scheme :: ZF_REFLE:sch 2

OrdSeqOfUnivEx{ F_{1}() -> Universe, P_{1}[ set , set ] } :

provided

OrdSeqOfUnivEx{ F

provided

proof end;

scheme :: ZF_REFLE:sch 3

UOSExist{ F_{1}() -> Universe, F_{2}() -> Ordinal of F_{1}(), F_{3}( Ordinal, Ordinal) -> Ordinal of F_{1}(), F_{4}( Ordinal, T-Sequence) -> Ordinal of F_{1}() } :

UOSExist{ F

ex phi being Ordinal-Sequence of F_{1}() st

( phi . (0-element_of F_{1}()) = F_{2}() & ( for a being Ordinal of F_{1}() holds phi . (succ a) = F_{3}(a,(phi . a)) ) & ( for a being Ordinal of F_{1}() st a <> 0-element_of F_{1}() & a is limit_ordinal holds

phi . a = F_{4}(a,(phi | a)) ) )

( phi . (0-element_of F

phi . a = F

proof end;

scheme :: ZF_REFLE:sch 4

UniverseInd{ F_{1}() -> Universe, P_{1}[ Ordinal] } :

provided

UniverseInd{ F

provided

A1:
P_{1}[ 0-element_of F_{1}()]
and

A2: for a being Ordinal of F_{1}() st P_{1}[a] holds

P_{1}[ succ a]
and

A3: for a being Ordinal of F_{1}() st a <> 0-element_of F_{1}() & a is limit_ordinal & ( for b being Ordinal of F_{1}() st b in a holds

P_{1}[b] ) holds

P_{1}[a]

A2: for a being Ordinal of F

P

A3: for a being Ordinal of F

P

P

proof end;

definition

let f be Function;

let W be Universe;

let a be Ordinal of W;

correctness

coherence

Union (W |` (f | (Rank a))) is set ;

;

end;
let W be Universe;

let a be Ordinal of W;

correctness

coherence

Union (W |` (f | (Rank a))) is set ;

;

:: deftheorem defines union ZF_REFLE:def 1 :

for f being Function

for W being Universe

for a being Ordinal of W holds union (f,a) = Union (W |` (f | (Rank a)));

for f being Function

for W being Universe

for a being Ordinal of W holds union (f,a) = Union (W |` (f | (Rank a)));

definition

let phi be Ordinal-Sequence;

let W be Universe;

let a be Ordinal of W;

:: original: union

redefine func union (phi,a) -> Ordinal of W;

coherence

union (phi,a) is Ordinal of W

end;
let W be Universe;

let a be Ordinal of W;

:: original: union

redefine func union (phi,a) -> Ordinal of W;

coherence

union (phi,a) is Ordinal of W

proof end;

theorem Th14: :: ZF_REFLE:14

for W being Universe

for a being Ordinal of W

for phi being Ordinal-Sequence of W holds

( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )

for a being Ordinal of W

for phi being Ordinal-Sequence of W holds

( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )

proof end;

definition

let W be Universe;

let a, b be Ordinal of W;

:: original: \/

redefine func a \/ b -> Ordinal of W;

coherence

a \/ b is Ordinal of W

end;
let a, b be Ordinal of W;

:: original: \/

redefine func a \/ b -> Ordinal of W;

coherence

a \/ b is Ordinal of W

proof end;

registration
end;

:: deftheorem Def2 defines DOMAIN-yielding ZF_REFLE:def 2 :

for W being Universe

for IT being T-Sequence of W holds

( IT is DOMAIN-yielding iff dom IT = On W );

for W being Universe

for IT being T-Sequence of W holds

( IT is DOMAIN-yielding iff dom IT = On W );

registration

let W be Universe;

existence

ex b_{1} being T-Sequence of W st

( b_{1} is DOMAIN-yielding & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

definition
end;

definition

let W be Universe;

let L be DOMAIN-Sequence of W;

:: original: Union

redefine func Union L -> Subclass of W;

coherence

Union L is Subclass of W

:: original: .

redefine func L . a -> non empty Element of W;

coherence

L . a is non empty Element of W

end;
let L be DOMAIN-Sequence of W;

:: original: Union

redefine func Union L -> Subclass of W;

coherence

Union L is Subclass of W

proof end;

let a be Ordinal of W;:: original: .

redefine func L . a -> non empty Element of W;

coherence

L . a is non empty Element of W

proof end;

theorem Th16: :: ZF_REFLE:16

for W being Universe

for a being Ordinal of W

for L being DOMAIN-Sequence of W holds L . a c= Union L

for a being Ordinal of W

for L being DOMAIN-Sequence of W holds L . a c= Union L

proof end;

:: Reflection Theorem

theorem :: ZF_REFLE:20

for W being Universe

for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

for H being ZF-formula ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

for f being Function of VAR,(L . a) holds

( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )

for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

for H being ZF-formula ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

for f being Function of VAR,(L . a) holds

( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )

proof end;

begin