let x be Surreal; for Inv being Function holds Union (divL (x,Inv)) = ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
let Inv be Function; Union (divL (x,Inv)) = ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
defpred S1[ Nat] means (divL (x,Inv)) . $1 c= ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv));
(divL (x,Inv)) . 0 = {0_No}
by Th1;
then A1:
S1[ 0 ]
by XBOOLE_1:7, XBOOLE_1:10;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
let o be
object ;
TARSKI:def 3 ( not o in (divL (x,Inv)) . (n + 1) or o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) )
assume A4:
o in (divL (x,Inv)) . (n + 1)
;
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
(divL (x,Inv)) . (n + 1) = (((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(L_ x),Inv))
by Th6;
then
(
o in ((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv)) or
o in divset (
((divR (x,Inv)) . n),
x,
(L_ x),
Inv) )
by A4, XBOOLE_0:def 3;
per cases then
( o in (divL (x,Inv)) . n or o in divset (((divL (x,Inv)) . n),x,(R_ x),Inv) or o in divset (((divR (x,Inv)) . n),x,(L_ x),Inv) )
by XBOOLE_0:def 3;
suppose A5:
o in divset (
((divL (x,Inv)) . n),
x,
(R_ x),
Inv)
;
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
divset (
((divL (x,Inv)) . n),
x,
(R_ x),
Inv)
c= divset (
(Union (divL (x,Inv))),
x,
(R_ x),
Inv)
by ABCMIZ_1:1, Th11;
then
o in {0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))
by A5, XBOOLE_0:def 3;
hence
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
by XBOOLE_0:def 3;
verum end; suppose A6:
o in divset (
((divR (x,Inv)) . n),
x,
(L_ x),
Inv)
;
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
divset (
((divR (x,Inv)) . n),
x,
(L_ x),
Inv)
c= divset (
(Union (divR (x,Inv))),
x,
(L_ x),
Inv)
by Th11, ABCMIZ_1:1;
hence
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
by A6, XBOOLE_0:def 3;
verum end;
end;
A7:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
thus
Union (divL (x,Inv)) c= ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
XBOOLE_0:def 10 ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) c= Union (divL (x,Inv))proof
let o be
object ;
TARSKI:def 3 ( not o in Union (divL (x,Inv)) or o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) )
assume
o in Union (divL (x,Inv))
;
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
then consider n being
object such that A8:
(
n in dom (divL (x,Inv)) &
o in (divL (x,Inv)) . n )
by CARD_5:2;
n in NAT
by A8, Def5;
then reconsider n =
n as
Nat ;
(divL (x,Inv)) . n c= ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
by A7;
hence
o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))
by A8;
verum
end;
A9:
divset ((Union (divL (x,Inv))),x,(R_ x),Inv) c= Union (divL (x,Inv))
proof
let o be
object ;
TARSKI:def 3 ( not o in divset ((Union (divL (x,Inv))),x,(R_ x),Inv) or o in Union (divL (x,Inv)) )
assume
o in divset (
(Union (divL (x,Inv))),
x,
(R_ x),
Inv)
;
o in Union (divL (x,Inv))
then consider l being
object such that A10:
(
l in Union (divL (x,Inv)) &
o in divs (
l,
x,
(R_ x),
Inv) )
by Def3;
consider n being
object such that A11:
(
n in dom (divL (x,Inv)) &
l in (divL (x,Inv)) . n )
by A10, CARD_5:2;
n in NAT
by A11, Def5;
then reconsider n =
n as
Nat ;
o in divset (
((divL (x,Inv)) . n),
x,
(R_ x),
Inv)
by A10, A11, Def3;
then
o in ((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))
by XBOOLE_0:def 3;
then
o in (((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(L_ x),Inv))
by XBOOLE_0:def 3;
then A12:
o in (divL (x,Inv)) . (n + 1)
by Th6;
n + 1
in NAT
;
then
n + 1
in dom (divL (x,Inv))
by Def5;
hence
o in Union (divL (x,Inv))
by A12, CARD_5:2;
verum
end;
A13:
divset ((Union (divR (x,Inv))),x,(L_ x),Inv) c= Union (divL (x,Inv))
proof
let o be
object ;
TARSKI:def 3 ( not o in divset ((Union (divR (x,Inv))),x,(L_ x),Inv) or o in Union (divL (x,Inv)) )
assume
o in divset (
(Union (divR (x,Inv))),
x,
(L_ x),
Inv)
;
o in Union (divL (x,Inv))
then consider l being
object such that A14:
(
l in Union (divR (x,Inv)) &
o in divs (
l,
x,
(L_ x),
Inv) )
by Def3;
consider n being
object such that A15:
(
n in dom (divR (x,Inv)) &
l in (divR (x,Inv)) . n )
by A14, CARD_5:2;
n in NAT
by A15, Def6;
then reconsider n =
n as
Nat ;
o in divset (
((divR (x,Inv)) . n),
x,
(L_ x),
Inv)
by A14, A15, Def3;
then
o in (((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(L_ x),Inv))
by XBOOLE_0:def 3;
then A16:
o in (divL (x,Inv)) . (n + 1)
by Th6;
n + 1
in NAT
;
then
n + 1
in dom (divL (x,Inv))
by Def5;
hence
o in Union (divL (x,Inv))
by A16, CARD_5:2;
verum
end;
(divL (x,Inv)) . 0 = {0_No}
by Th1;
then
{0_No} c= Union (divL (x,Inv))
by ABCMIZ_1:1;
then
{0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv)) c= Union (divL (x,Inv))
by A9, XBOOLE_1:8;
hence
({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) c= Union (divL (x,Inv))
by A13, XBOOLE_1:8; verum