let phi, psi be Ordinal-Sequence; ( rng phi = rng psi & phi is increasing & psi is increasing implies for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A ) )
assume that
A1:
rng phi = rng psi
and
A2:
phi is increasing
; ( not psi is increasing or for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A ) )
defpred S1[ Ordinal] means ( $1 in dom phi implies ( $1 in dom psi & phi . $1 = psi . $1 ) );
assume A3:
for A, B being Ordinal st A in B & B in dom psi holds
psi . A in psi . B
; ORDINAL2:def 12 for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
A4:
for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be
Ordinal;
( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that A5:
for
B being
Ordinal st
B in A &
B in dom phi holds
(
B in dom psi &
phi . B = psi . B )
and A6:
A in dom phi
;
( A in dom psi & phi . A = psi . A )
phi . A in rng phi
by A6, FUNCT_1:def 3;
then consider x being
object such that A7:
x in dom psi
and A8:
phi . A = psi . x
by A1, FUNCT_1:def 3;
reconsider x =
x as
Ordinal by A7;
A9:
now not A in xassume A10:
A in x
;
contradictionthen A11:
A in dom psi
by A7, ORDINAL1:10;
then
psi . A in rng psi
by FUNCT_1:def 3;
then consider y being
object such that A12:
y in dom phi
and A13:
psi . A = phi . y
by A1, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A12;
psi . A in psi . x
by A3, A7, A10;
then
not
A c= y
by A2, A8, A12, A13, ORDINAL1:5, ORDINAL4:9;
then A14:
y in A
by ORDINAL1:16;
then A15:
psi . y = phi . y
by A5, A12;
psi . y in psi . A
by A3, A11, A14;
hence
contradiction
by A13, A15;
verum end;
hence
(
A in dom psi &
phi . A = psi . A )
by A7, A8, A9, ORDINAL1:14;
verum
end;
thus
for A being Ordinal holds S1[A]
from ORDINAL1:sch 2(A4); verum