let X be set ; for S being SigmaField of X
for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
union (rng G) = (F . 0) \ (meet (rng F))
let S be SigmaField of X; for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
union (rng G) = (F . 0) \ (meet (rng F))
let G, F be sequence of S; ( G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies union (rng G) = (F . 0) \ (meet (rng F)) )
assume that
A1:
G . 0 = {}
and
A2:
for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n )
; union (rng G) = (F . 0) \ (meet (rng F))
A3:
dom G = NAT
by FUNCT_2:def 1;
thus
union (rng G) c= (F . 0) \ (meet (rng F))
XBOOLE_0:def 10 (F . 0) \ (meet (rng F)) c= union (rng G)proof
let A be
object ;
TARSKI:def 3 ( not A in union (rng G) or A in (F . 0) \ (meet (rng F)) )
assume
A in union (rng G)
;
A in (F . 0) \ (meet (rng F))
then consider Z being
set such that A4:
A in Z
and A5:
Z in rng G
by TARSKI:def 4;
consider n being
object such that A6:
n in NAT
and A7:
Z = G . n
by A3, A5, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A6;
consider k being
Nat such that A8:
n = k + 1
by A1, A4, A7, NAT_1:6;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
set Y =
F . k;
A9:
A in (F . 0) \ (F . k)
by A2, A4, A7, A8;
then
(
F . k in rng F & not
A in F . k )
by FUNCT_2:4, XBOOLE_0:def 5;
then A10:
not
A in meet (rng F)
by SETFAM_1:def 1;
A in F . 0
by A9, XBOOLE_0:def 5;
hence
A in (F . 0) \ (meet (rng F))
by A10, XBOOLE_0:def 5;
verum
end;
let A be object ; TARSKI:def 3 ( not A in (F . 0) \ (meet (rng F)) or A in union (rng G) )
assume A11:
A in (F . 0) \ (meet (rng F))
; A in union (rng G)
then
not A in meet (rng F)
by XBOOLE_0:def 5;
then A12:
ex Y being set st
( Y in rng F & not A in Y )
by SETFAM_1:def 1;
A in F . 0
by A11, XBOOLE_0:def 5;
then consider Y being set such that
A13:
A in F . 0
and
A14:
Y in rng F
and
A15:
not A in Y
by A12;
dom F = NAT
by FUNCT_2:def 1;
then consider n being object such that
A16:
n in NAT
and
A17:
Y = F . n
by A14, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A16;
A in (F . 0) \ (F . n)
by A13, A15, A17, XBOOLE_0:def 5;
then A18:
A in G . (n + 1)
by A2;
G . (n + 1) in rng G
by FUNCT_2:4;
hence
A in union (rng G)
by A18, TARSKI:def 4; verum