:: by Grzegorz Bancerek

::

:: Received March 1, 1990

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: ORDINAL3:1

theorem :: ORDINAL3:2

proof end;

theorem :: ORDINAL3:3

canceled;

theorem :: ORDINAL3:4

canceled;

theorem :: ORDINAL3:5

proof end;

theorem :: ORDINAL3:6

proof end;

theorem Th7: :: ORDINAL3:7

proof end;

theorem Th8: :: ORDINAL3:8

proof end;

theorem Th9: :: ORDINAL3:9

proof end;

theorem Th10: :: ORDINAL3:10

proof end;

theorem :: ORDINAL3:11

proof end;

theorem :: ORDINAL3:12

proof end;

theorem :: ORDINAL3:13

proof end;

registration

let A, B be Ordinal;

cluster A \/ B -> ordinal ;

coherence

A \/ B is ordinal

coherence

A /\ B is ordinal

end;
cluster A \/ B -> ordinal ;

coherence

A \/ B is ordinal

proof end;

cluster A /\ B -> ordinal ;coherence

A /\ B is ordinal

proof end;

theorem :: ORDINAL3:14

canceled;

theorem :: ORDINAL3:15

proof end;

theorem :: ORDINAL3:16

proof end;

Lm1: 1 = succ {}

;

theorem Th17: :: ORDINAL3:17

proof end;

theorem :: ORDINAL3:18

theorem Th19: :: ORDINAL3:19

proof end;

theorem :: ORDINAL3:20

proof end;

theorem :: ORDINAL3:21

proof end;

theorem Th22: :: ORDINAL3:22

proof end;

theorem :: ORDINAL3:23

proof end;

theorem Th24: :: ORDINAL3:24

proof end;

theorem Th25: :: ORDINAL3:25

proof end;

theorem Th26: :: ORDINAL3:26

proof end;

theorem Th27: :: ORDINAL3:27

proof end;

theorem :: ORDINAL3:28

proof end;

theorem Th29: :: ORDINAL3:29

proof end;

theorem Th30: :: ORDINAL3:30

proof end;

theorem Th31: :: ORDINAL3:31

proof end;

theorem Th32: :: ORDINAL3:32

proof end;

theorem Th33: :: ORDINAL3:33

proof end;

theorem :: ORDINAL3:34

proof end;

theorem :: ORDINAL3:35

proof end;

theorem Th36: :: ORDINAL3:36

proof end;

theorem Th37: :: ORDINAL3:37

proof end;

theorem Th38: :: ORDINAL3:38

proof end;

theorem Th39: :: ORDINAL3:39

proof end;

theorem :: ORDINAL3:40

canceled;

theorem :: ORDINAL3:41

proof end;

theorem Th42: :: ORDINAL3:42

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;

canceled;

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

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

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

existence

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}

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

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

existence

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}

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

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

existence

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}

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

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

existence

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;

canceled;

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

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

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

existence

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func fi +^ C -> Ordinal-Sequence means :: ORDINAL3:def 3( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

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

existence

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func C *^ fi -> Ordinal-Sequence means :: ORDINAL3:def 4( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

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

existence

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func fi *^ C -> Ordinal-Sequence means :Def5: :: ORDINAL3:def 5( dom it = dom fi & ( for A being Ordinal st A in dom fi holds

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

existence

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem ORDINAL3:def 1 :

canceled;

:: deftheorem Def2 defines +^ ORDINAL3:def 2 :

for C being Ordinal

for fi, b

( b

b

:: deftheorem defines +^ ORDINAL3:def 3 :

for C being Ordinal

for fi, b

( b

b

:: deftheorem defines *^ ORDINAL3:def 4 :

for C being Ordinal

for fi, b

( b

b

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

for C being Ordinal

for fi, b

( b

b

theorem :: ORDINAL3:43

canceled;

theorem :: ORDINAL3:44

canceled;

theorem :: ORDINAL3:45

canceled;

theorem :: ORDINAL3:46

canceled;

theorem Th47: :: ORDINAL3:47

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 Th48: :: ORDINAL3:48

proof end;

theorem Th49: :: ORDINAL3:49

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 Th50: :: ORDINAL3:50

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 Th51: :: ORDINAL3:51

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 Th52: :: ORDINAL3:52

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 Th53: :: ORDINAL3:53

proof end;

theorem Th54: :: ORDINAL3:54

proof end;

theorem Th55: :: ORDINAL3:55

proof end;

theorem Th56: :: ORDINAL3:56

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 Th57: :: ORDINAL3:57

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;

theorem :: ORDINAL3:58

proof end;

definition

let A, B be Ordinal;

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

A = B +^ it if B c= A

otherwise it = {} ;

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 Th30;

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 Th24;

consistency

for b_{1} being Ordinal holds verum
;

func A div^ B -> Ordinal means :Def7: :: ORDINAL3:def 7

ex C being Ordinal st

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

otherwise it = {} ;

consistency

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 Th55;

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 Th56;

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

A = B +^ it if B c= A

otherwise it = {} ;

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 :Def7: :: ORDINAL3:def 7

ex C being Ordinal st

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

otherwise it = {} ;

consistency

for b

existence

( ( B <> {} implies ex b

( A = (b

uniqueness

for b

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

( A = (b

( A = (b

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

for A, B, b

( ( B c= A implies ( b

:: deftheorem Def7 defines div^ ORDINAL3:def 7 :

for A, B, b

( ( B <> {} implies ( b

( A = (b

definition

let A, B be Ordinal;

func A mod^ B -> Ordinal equals :: ORDINAL3:def 8

A -^ ((A div^ B) *^ B);

correctness

coherence

A -^ ((A div^ B) *^ B) is Ordinal;

;

end;
func A mod^ B -> Ordinal equals :: ORDINAL3:def 8

A -^ ((A div^ B) *^ B);

correctness

coherence

A -^ ((A div^ B) *^ B) is Ordinal;

;

:: deftheorem defines mod^ ORDINAL3:def 8 :

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

theorem :: ORDINAL3:59

canceled;

theorem :: ORDINAL3:60

proof end;

theorem :: ORDINAL3:61

canceled;

theorem :: ORDINAL3:62

canceled;

theorem :: ORDINAL3:63

canceled;

theorem :: ORDINAL3:64

canceled;

theorem Th65: :: ORDINAL3:65

proof end;

theorem Th66: :: ORDINAL3:66

proof end;

theorem Th67: :: ORDINAL3:67

proof end;

theorem :: ORDINAL3:68

proof end;

theorem Th69: :: ORDINAL3:69

proof end;

theorem :: ORDINAL3:70

proof end;

theorem :: ORDINAL3:71

proof end;

theorem :: ORDINAL3:72

proof end;

theorem :: ORDINAL3:73

proof end;

theorem :: ORDINAL3:74

proof end;

theorem :: ORDINAL3:75

proof end;

theorem :: ORDINAL3:76

proof end;

theorem Th77: :: ORDINAL3:77

proof end;

theorem Th78: :: ORDINAL3:78

proof end;

theorem :: ORDINAL3:79

proof end;

theorem :: ORDINAL3:80

proof end;

theorem Th81: :: ORDINAL3:81

proof end;

theorem :: ORDINAL3:82

proof end;

theorem :: ORDINAL3:83

proof end;

theorem :: ORDINAL3:84

proof end;

begin

theorem :: ORDINAL3:85

proof end;

theorem :: ORDINAL3:86

proof end;

theorem Th87: :: ORDINAL3:87

proof end;

registration

let a, b be natural Ordinal;

cluster a -^ b -> natural ;

coherence

a -^ b is natural

coherence

a *^ b is natural

end;
cluster a -^ b -> natural ;

coherence

a -^ b is natural

proof end;

cluster a *^ b -> natural ;coherence

a *^ b is natural

proof end;

theorem :: ORDINAL3:88

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;