ORDINAL3: Ordinal Arithmetics

:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem :: ORDINAL3:1

for X being set holds X c= succ X by XBOOLE_1:7;

theorem :: ORDINAL3:2

for X, Y being set st succ X c= Y holds
X c= Y

proof end;

theorem :: ORDINAL3:3

for A, B being Ordinal holds
( A in B iff succ A in succ B )

proof end;

theorem :: ORDINAL3:4

for A being Ordinal
for X being set st X c= A holds
union X is epsilon-transitive epsilon-connected set

proof end;

theorem Th5: :: ORDINAL3:5

for X being set holds union (On X) is epsilon-transitive epsilon-connected set

proof end;

theorem Th6: :: ORDINAL3:6

for A being Ordinal
for X being set st X c= A holds
On X = X

proof end;

theorem Th7: :: ORDINAL3:7

for A being Ordinal holds On {A} = {A}

proof end;

theorem Th8: :: ORDINAL3:8

for A being Ordinal st A <> {} holds
{} in A

proof end;

theorem :: ORDINAL3:9

for A being Ordinal holds inf A = {}

proof end;

theorem :: ORDINAL3:10

for A being Ordinal holds inf {A} = A

proof end;

theorem :: ORDINAL3:11

for A being Ordinal
for X being set st X c= A holds
meet X is Ordinal

proof end;

registration

let A, B be Ordinal;

cluster A \/ B -> ordinal ;

proof end;

cluster A /\ B -> ordinal ;

proof end;

end;

theorem :: ORDINAL3:12

for A, B being Ordinal holds
( A \/ B = A or A \/ B = B )

proof end;

theorem :: ORDINAL3:13

for A, B being Ordinal holds
( A /\ B = A or A /\ B = B )

proof end;

Lm1: 1 = succ 0
;

theorem Th14: :: ORDINAL3:14

for A being Ordinal st A in 1 holds
A = {}

proof end;

theorem :: ORDINAL3:15

1 = {{}} by Lm1;

theorem Th16: :: ORDINAL3:16

for A being Ordinal holds
( not A c= 1 or A = {} or A = 1 )

proof end;

theorem :: ORDINAL3:17

for A, B, C, D being Ordinal st ( A c= B or A in B ) & C in D holds
A +^ C in B +^ D

proof end;

theorem :: ORDINAL3:18

for A, B, C, D being Ordinal st A c= B & C c= D holds
A +^ C c= B +^ D

proof end;

theorem Th19: :: ORDINAL3:19

for A, B, C, D being Ordinal st A in B & ( ( C c= D & D <> {} ) or C in D ) holds
A *^ C in B *^ D

proof end;

theorem :: ORDINAL3:20

for A, B, C, D being Ordinal st A c= B & C c= D holds
A *^ C c= B *^ D

proof end;

theorem Th21: :: ORDINAL3:21

for B, C, D being Ordinal st B +^ C = B +^ D holds
C = D

proof end;

theorem Th22: :: ORDINAL3:22

for B, C, D being Ordinal st B +^ C in B +^ D holds
C in D

proof end;

theorem Th23: :: ORDINAL3:23

for B, C, D being Ordinal st B +^ C c= B +^ D holds
C c= D

proof end;

theorem Th24: :: ORDINAL3:24

for A, B being Ordinal holds
( A c= A +^ B & B c= A +^ B )

proof end;

theorem :: ORDINAL3:25

for A, B, C being Ordinal st A in B holds
( A in B +^ C & A in C +^ B )

proof end;

theorem Th26: :: ORDINAL3:26

for A, B being Ordinal st A +^ B = {} holds
( A = {} & B = {} ) by Th24, XBOOLE_1:3;

theorem Th27: :: ORDINAL3:27

for A, B being Ordinal st A c= B holds
ex C being Ordinal st B = A +^ C

proof end;

theorem Th28: :: ORDINAL3:28

for A, B being Ordinal st A in B holds
ex C being Ordinal st
( B = A +^ C & C <> {} )

proof end;

theorem Th29: :: ORDINAL3:29

for A, B being Ordinal st A <> {} & A is limit_ordinal holds
B +^ A is limit_ordinal

proof end;

theorem Th30: :: ORDINAL3:30

for A, B, C being Ordinal holds (A +^ B) +^ C = A +^ (B +^ C)

proof end;

theorem :: ORDINAL3:31

for A, B being Ordinal holds
( not A *^ B = {} or A = {} or B = {} )

proof end;

theorem :: ORDINAL3:32

for A, B, C being Ordinal st A in B & C <> {} holds
( A in B *^ C & A in C *^ B )

proof end;

theorem Th33: :: ORDINAL3:33

for A, B, C being Ordinal st B *^ A = C *^ A & A <> {} holds
B = C

proof end;

theorem Th34: :: ORDINAL3:34

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

proof end;

theorem Th35: :: ORDINAL3:35

for A, B, C being Ordinal st B *^ A c= C *^ A & A <> {} holds
B c= C

proof end;

theorem Th36: :: ORDINAL3:36

for A, B being Ordinal st B <> {} holds
( A c= A *^ B & A c= B *^ A )

proof end;

theorem :: ORDINAL3:37

for A, B being Ordinal st A *^ B = 1 holds
( A = 1 & B = 1 )

proof end;

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 ) )

proof end;

definition

let C be Ordinal;
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) ) );

proof end;

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

proof end;

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

proof end;

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

proof end;

proof end;

end;

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

:: deftheorem defines +^ ORDINAL3:def 2 :

:: deftheorem defines *^ ORDINAL3:def 3 :

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

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)

proof end;

theorem Th40: :: ORDINAL3:40

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

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 )

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

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)

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

proof end;

theorem Th45: :: ORDINAL3:45

for A, B being Ordinal st B <> {} holds
union (A +^ B) = A +^ (union B)

proof end;

theorem Th46: :: ORDINAL3:46

for A, B, C being Ordinal holds (A +^ B) *^ C = (A *^ C) +^ (B *^ C)

proof end;

theorem Th47: :: ORDINAL3:47

for A, B being Ordinal st A <> {} holds
ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )

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 )

proof end;

theorem Th49: :: ORDINAL3:49

for A, B 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

proof end;

theorem :: ORDINAL3:50

for A, B, C being Ordinal holds (A *^ B) *^ C = A *^ (B *^ C)

proof end;

definition

let A, B be Ordinal;

func A -^ B -> Ordinal means :Def5: :: ORDINAL3:def 5
A = B +^ it if B c= A
otherwise it = {} ;

existence by Th27;
uniqueness by Th21;
consistency ;

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 ;
existence by Th47;
uniqueness by Th48;

end;

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

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

definition

let A, B be Ordinal;

func A mod^ B -> Ordinal equals :: ORDINAL3:def 7
A -^ ((A div^ B) *^ B);

end;

:: deftheorem defines mod^ ORDINAL3:def 7 :

theorem :: ORDINAL3:51

for A, B being Ordinal st A in B holds
B = A +^ (B -^ A)

proof end;

theorem Th52: :: ORDINAL3:52

for A, B being Ordinal holds (A +^ B) -^ A = B

proof end;

theorem Th53: :: ORDINAL3:53

for A, B, C being Ordinal st A in B & ( C c= A or C in A ) holds
A -^ C in B -^ C

proof end;

theorem Th54: :: ORDINAL3:54

for A being Ordinal holds A -^ A = {}

proof end;

theorem :: ORDINAL3:55

for A, B being Ordinal st A in B holds
( B -^ A <> {} & {} in B -^ A )

proof end;

theorem Th56: :: ORDINAL3:56

for A being Ordinal holds
( A -^ {} = A & {} -^ A = {} )

proof end;

theorem :: ORDINAL3:57

for A, B, C being Ordinal holds A -^ (B +^ C) = (A -^ B) -^ C

proof end;

theorem :: ORDINAL3:58

for A, B, C being Ordinal st A c= B holds
C -^ B c= C -^ A

proof end;

theorem :: ORDINAL3:59

for A, B, C being Ordinal st A c= B holds
A -^ C c= B -^ C

proof end;

theorem :: ORDINAL3:60

for A, B, C being Ordinal st C <> {} & A in B +^ C holds
A -^ B in C

proof end;

theorem :: ORDINAL3:61

for A, B, C being Ordinal st A +^ B in C holds
B in C -^ A

proof end;

theorem :: ORDINAL3:62

for A, B being Ordinal holds A c= B +^ (A -^ B)

proof end;

theorem :: ORDINAL3:63

for A, B, C being Ordinal holds (A *^ C) -^ (B *^ C) = (A -^ B) *^ C

proof end;

theorem Th64: :: ORDINAL3:64

for A, B being Ordinal holds (A div^ B) *^ B c= A

proof end;

theorem Th65: :: ORDINAL3:65

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

proof end;

theorem :: ORDINAL3:66

for A, B, C, D being Ordinal st A = (B *^ C) +^ D & D in C holds
( B = A div^ C & D = A mod^ C )

proof end;

theorem :: ORDINAL3:67

for A, B, C being Ordinal st A in B *^ C holds
( A div^ C in B & A mod^ C in C )

proof end;

theorem Th68: :: ORDINAL3:68

for A, B being Ordinal st B <> {} holds
(A *^ B) div^ B = A

proof end;

theorem :: ORDINAL3:69

for A, B being Ordinal holds (A *^ B) mod^ B = {}

proof end;

theorem :: ORDINAL3:70

for A being Ordinal holds
( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )

proof end;

theorem :: ORDINAL3:71

for A being Ordinal holds
( A div^ 1 = A & A mod^ 1 = {} )

proof end;

:: from ZF_REFLE, 2007.03.13, A.T.

theorem :: ORDINAL3:72

for X being set holds sup X c= succ (union (On X))

proof end;

theorem :: ORDINAL3:73

for A being Ordinal holds succ A is_cofinal_with 1

proof end;

:: from ARYTM_3, 2007.10.23, A.T.

theorem Th74: :: ORDINAL3:74

for a, b being Ordinal st a +^ b is natural holds
( a in omega & b in omega ) by Th24, ORDINAL1:12;

registration

let a, b be natural Ordinal;

cluster a -^ b -> natural ;

proof end;

cluster a *^ b -> natural ;

proof end;

end;

theorem :: ORDINAL3:75

for a, b being Ordinal st a *^ b is natural & not a *^ b is empty holds
( a in omega & b in omega )

proof end;

definition

let a, b be natural Ordinal;
:: original: +^
redefine func a +^ b -> set ;
commutativity

proof end;

end;

definition

let a, b be natural Ordinal;
:: original: *^
redefine func a *^ b -> set ;
commutativity

proof end;

end;