set f = U exp a;
A1:
dom (U exp a) = On U
by FUNCT_2:def 1;
A2:
0 in a
by ORDINAL3:8;
succ 0 c= a
;
then
1 c< a
;
then A3:
1 in a
by ORDINAL1:11;
hence
U exp a is increasing
by A3, ORDINAL5:10; ORDINAL6:def 3 U exp a is continuous
let b be Ordinal; ORDINAL2:def 13 for b1 being set holds
( not b in dom (U exp a) or b = 0 or not b is limit_ordinal or not b1 = (U exp a) . b or b1 is_limes_of (U exp a) | b )
let c be Ordinal; ( not b in dom (U exp a) or b = 0 or not b is limit_ordinal or not c = (U exp a) . b or c is_limes_of (U exp a) | b )
assume A5:
( b in dom (U exp a) & b <> 0 & b is limit_ordinal & c = (U exp a) . b )
; c is_limes_of (U exp a) | b
then
b c= dom (U exp a)
by ORDINAL1:def 2;
then A6:
dom ((U exp a) | b) = b
by RELAT_1:62;
A7:
(U exp a) | b is increasing
by A4, A3, ORDINAL4:15, ORDINAL5:10;
A8:
b in U
by A1, A5, ORDINAL1:def 9;
then A9:
(U exp a) . b = exp (a,b)
by Def8;
(U exp a) . b = Union ((U exp a) | b)
proof
thus
(U exp a) . b c= Union ((U exp a) | b)
XBOOLE_0:def 10 Union ((U exp a) | b) c= (U exp a) . bproof
let c be
Ordinal;
ORDINAL1:def 5 ( not c in (U exp a) . b or c in Union ((U exp a) | b) )
assume
c in (U exp a) . b
;
c in Union ((U exp a) | b)
then consider d being
Ordinal such that A10:
(
d in b &
c in exp (
a,
d) )
by A2, A5, A9, ORDINAL5:11;
d in U
by A8, A10, ORDINAL1:10;
then exp (
a,
d) =
(U exp a) . d
by Def8
.=
((U exp a) | b) . d
by A10, FUNCT_1:49
;
hence
c in Union ((U exp a) | b)
by A6, A10, CARD_5:2;
verum
end;
let c be
Ordinal;
ORDINAL1:def 5 ( not c in Union ((U exp a) | b) or c in (U exp a) . b )
assume
c in Union ((U exp a) | b)
;
c in (U exp a) . b
then consider x being
object such that A11:
(
x in b &
c in ((U exp a) | b) . x )
by A6, CARD_5:2;
reconsider x =
x as
Ordinal by A11;
x in U
by A8, A11, ORDINAL1:10;
then exp (
a,
x) =
(U exp a) . x
by Def8
.=
((U exp a) | b) . x
by A11, FUNCT_1:49
;
hence
c in (U exp a) . b
by A2, A11, A5, A9, ORDINAL5:11;
verum
end;
hence
c is_limes_of (U exp a) | b
by A5, A7, A6, ORDINAL5:6; verum