hereby ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 )
assume A1:
( 1
in b &
0 in a )
;
ex c being Ordinal st
( exp (b,c) c= a & ( for d being Ordinal st exp (b,d) c= a holds
not d c/= c ) )defpred S1[
Ordinal]
means a c= exp (
b,$1);
a c= exp (
b,
a)
by A1, ORDINAL4:32;
then A2:
ex
c being
Ordinal st
S1[
c]
;
consider c being
Ordinal such that A3:
(
S1[
c] & ( for
d being
Ordinal st
S1[
d] holds
c c= d ) )
from ORDINAL1:sch 1(A2);
0 in Segm 1
by NAT_1:44;
then A4:
0 in b
by A1, ORDINAL1:10;
per cases
( a = exp (b,c) or a c< exp (b,c) )
by A3;
suppose A7:
a c< exp (
b,
c)
;
ex d being Ordinal st
( exp (b,d) c= a & ( for e being Ordinal st exp (b,e) c= a holds
not e c/= d ) )then A8:
a in exp (
b,
c)
by ORDINAL1:11;
succ 0 c= a
by A1, ORDINAL1:21;
then
( 1
in exp (
b,
c) &
exp (
b,
0)
= 1 )
by A7, ORDINAL1:11, ORDINAL1:12, ORDINAL2:43;
then A9:
c <> 0
;
then consider d being
Ordinal such that A11:
c = succ d
by ORDINAL1:29;
take d =
d;
( exp (b,d) c= a & ( for e being Ordinal st exp (b,e) c= a holds
not e c/= d ) )thus
exp (
b,
d)
c= a
for e being Ordinal st exp (b,e) c= a holds
not e c/= dlet e be
Ordinal;
( exp (b,e) c= a implies not e c/= d )assume A12:
(
exp (
b,
e)
c= a &
e c/= d )
;
contradictionthen
d in e
by ORDINAL1:16;
then
c c= e
by A11, ORDINAL1:21;
then
exp (
b,
c)
c= exp (
b,
e)
by A1, ORDINAL4:27;
then
a in exp (
b,
e)
by A8;
then
a in a
by A12;
hence
contradiction
;
verum end; end;
end;
thus
( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 )
; verum