:: by Grzegorz Bancerek

::

:: Received March 1, 1990

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

begin

registration
end;

Lm1: 1 = succ {}

;

theorem Th38: :: ORDINAL3:38

for A, B, C being Ordinal holds

( not A in B +^ C or A in B or ex D being Ordinal st

( D in C & A = B +^ D ) )

( not A in B +^ C or A in B or ex D being Ordinal st

( D in C & A = B +^ D ) )

proof end;

definition

let C be Ordinal;

let fi be Ordinal-Sequence;

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = C +^ (fi . A) ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = C +^ (fi . A) ) & dom b_{2} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{2} . A = C +^ (fi . A) ) holds

b_{1} = b_{2}

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = (fi . A) +^ C ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = (fi . A) +^ C ) & dom b_{2} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{2} . A = (fi . A) +^ C ) holds

b_{1} = b_{2}

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = C *^ (fi . A) ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = C *^ (fi . A) ) & dom b_{2} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{2} . A = C *^ (fi . A) ) holds

b_{1} = b_{2}

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = (fi . A) *^ C ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{1} . A = (fi . A) *^ C ) & dom b_{2} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{2} . A = (fi . A) *^ C ) holds

b_{1} = b_{2}

end;
let fi be Ordinal-Sequence;

func C +^ fi -> Ordinal-Sequence means :Def1: :: ORDINAL3:def 1

( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = C +^ (fi . A) ) );

existence ( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = C +^ (fi . A) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func fi +^ C -> Ordinal-Sequence means :: ORDINAL3:def 2

( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = (fi . A) +^ C ) );

existence ( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = (fi . A) +^ C ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func C *^ fi -> Ordinal-Sequence means :: ORDINAL3:def 3

( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = C *^ (fi . A) ) );

existence ( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = C *^ (fi . A) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func fi *^ C -> Ordinal-Sequence means :Def4: :: ORDINAL3:def 4

( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = (fi . A) *^ C ) );

existence ( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

it . A = (fi . A) *^ C ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines +^ ORDINAL3:def 1 :

for C being Ordinal

for fi, b_{3} being Ordinal-Sequence holds

( b_{3} = C +^ fi iff ( dom b_{3} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{3} . A = C +^ (fi . A) ) ) );

for C being Ordinal

for fi, b

( b

b

:: deftheorem defines +^ ORDINAL3:def 2 :

for C being Ordinal

for fi, b_{3} being Ordinal-Sequence holds

( b_{3} = fi +^ C iff ( dom b_{3} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{3} . A = (fi . A) +^ C ) ) );

for C being Ordinal

for fi, b

( b

b

:: deftheorem defines *^ ORDINAL3:def 3 :

for C being Ordinal

for fi, b_{3} being Ordinal-Sequence holds

( b_{3} = C *^ fi iff ( dom b_{3} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{3} . A = C *^ (fi . A) ) ) );

for C being Ordinal

for fi, b

( b

b

:: deftheorem Def4 defines *^ ORDINAL3:def 4 :

for C being Ordinal

for fi, b_{3} being Ordinal-Sequence holds

( b_{3} = fi *^ C iff ( dom b_{3} = dom fi & ( for A being Ordinal st A in dom fi holds

b_{3} . A = (fi . A) *^ C ) ) );

for C being Ordinal

for fi, b

( b

b

theorem Th39: :: ORDINAL3:39

for fi, psi being Ordinal-Sequence

for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds

psi . A = C +^ B ) holds

sup psi = C +^ (sup fi)

for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds

psi . A = C +^ B ) holds

sup psi = C +^ (sup fi)

proof end;

theorem Th41: :: ORDINAL3:41

for A, B, C being Ordinal st A in B *^ C & B is limit_ordinal holds

ex D being Ordinal st

( D in B & A in D *^ C )

ex D being Ordinal st

( D in B & A in D *^ C )

proof end;

theorem Th42: :: ORDINAL3:42

for fi, psi being Ordinal-Sequence

for C being Ordinal st dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds

psi . A = B *^ C ) holds

sup psi = (sup fi) *^ C

for C being Ordinal st dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds

psi . A = B *^ C ) holds

sup psi = (sup fi) *^ C

proof end;

theorem Th43: :: ORDINAL3:43

for fi being Ordinal-Sequence

for C being Ordinal st {} <> dom fi holds

sup (C +^ fi) = C +^ (sup fi)

for C being Ordinal st {} <> dom fi holds

sup (C +^ fi) = C +^ (sup fi)

proof end;

theorem Th44: :: ORDINAL3:44

for fi being Ordinal-Sequence

for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds

sup (fi *^ C) = (sup fi) *^ C

for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds

sup (fi *^ C) = (sup fi) *^ C

proof end;

theorem Th48: :: ORDINAL3:48

for A, C1, D1, C2, D2 being Ordinal st (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A holds

( C1 = C2 & D1 = D2 )

( C1 = C2 & D1 = D2 )

proof end;

theorem Th49: :: ORDINAL3:49

for B, A being Ordinal st 1 in B & A <> {} & A is limit_ordinal holds

for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds

fi . C = C *^ B ) holds

A *^ B = sup fi

for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds

fi . C = C *^ B ) holds

A *^ B = sup fi

proof end;

definition

let A, B be Ordinal;

existence

( ( B c= A implies ex b_{1} being Ordinal st A = B +^ b_{1} ) & ( not B c= A implies ex b_{1} being Ordinal st b_{1} = {} ) )
by Th27;

uniqueness

for b_{1}, b_{2} being Ordinal holds

( ( B c= A & A = B +^ b_{1} & A = B +^ b_{2} implies b_{1} = b_{2} ) & ( not B c= A & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )
by Th21;

consistency

for b_{1} being Ordinal holds verum
;

for b_{1} being Ordinal holds verum
;

existence

( ( B <> {} implies ex b_{1}, C being Ordinal st

( A = (b_{1} *^ B) +^ C & C in B ) ) & ( not B <> {} implies ex b_{1} being Ordinal st b_{1} = {} ) )
by Th47;

uniqueness

for b_{1}, b_{2} being Ordinal holds

( ( B <> {} & ex C being Ordinal st

( A = (b_{1} *^ B) +^ C & C in B ) & ex C being Ordinal st

( A = (b_{2} *^ B) +^ C & C in B ) implies b_{1} = b_{2} ) & ( not B <> {} & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )
by Th48;

end;
existence

( ( B c= A implies ex b

uniqueness

for b

( ( B c= A & A = B +^ b

consistency

for b

func A div^ B -> Ordinal means :Def6: :: ORDINAL3:def 6

ex C being Ordinal st

( A = (it *^ B) +^ C & C in B ) if B <> {}

otherwise it = {} ;

consistency ex C being Ordinal st

( A = (it *^ B) +^ C & C in B ) if B <> {}

otherwise it = {} ;

for b

existence

( ( B <> {} implies ex b

( A = (b

uniqueness

for b

( ( B <> {} & ex C being Ordinal st

( A = (b

( A = (b

:: deftheorem Def5 defines -^ ORDINAL3:def 5 :

for A, B, b_{3} being Ordinal holds

( ( B c= A implies ( b_{3} = A -^ B iff A = B +^ b_{3} ) ) & ( not B c= A implies ( b_{3} = A -^ B iff b_{3} = {} ) ) );

for A, B, b

( ( B c= A implies ( b

:: deftheorem Def6 defines div^ ORDINAL3:def 6 :

for A, B, b_{3} being Ordinal holds

( ( B <> {} implies ( b_{3} = A div^ B iff ex C being Ordinal st

( A = (b_{3} *^ B) +^ C & C in B ) ) ) & ( not B <> {} implies ( b_{3} = A div^ B iff b_{3} = {} ) ) );

for A, B, b

( ( B <> {} implies ( b

( A = (b

:: deftheorem defines mod^ ORDINAL3:def 7 :

for A, B being Ordinal holds A mod^ B = A -^ ((A div^ B) *^ B);

for A, B being Ordinal holds A mod^ B = A -^ ((A div^ B) *^ B);

begin

:: from ZF_REFLE, 2007.03.13, A.T.

:: from ARYTM_3, 2007.10.23, A.T.

registration

let a, b be natural Ordinal;

coherence

a -^ b is natural

a *^ b is natural

end;
coherence

a -^ b is natural

proof end;

coherence a *^ b is natural

proof end;

definition

let a, b be natural Ordinal;

:: original: +^

redefine func a +^ b -> set ;

commutativity

for a, b being natural Ordinal holds a +^ b = b +^ a

end;
:: original: +^

redefine func a +^ b -> set ;

commutativity

for a, b being natural Ordinal holds a +^ b = b +^ a

proof end;

definition

let a, b be natural Ordinal;

:: original: *^

redefine func a *^ b -> set ;

commutativity

for a, b being natural Ordinal holds a *^ b = b *^ a

end;
:: original: *^

redefine func a *^ b -> set ;

commutativity

for a, b being natural Ordinal holds a *^ b = b *^ a

proof end;