let X be set ; :: thesis: for B being SetSequence of X

for f being Function st dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) holds

f is SetSequence of X

let B be SetSequence of X; :: thesis: for f being Function st dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) holds

f is SetSequence of X

let f be Function; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) implies f is SetSequence of X )

assume that

A1: dom f = NAT and

A2: for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ; :: thesis: f is SetSequence of X

rng f c= bool X

for f being Function st dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) holds

f is SetSequence of X

let B be SetSequence of X; :: thesis: for f being Function st dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) holds

f is SetSequence of X

let f be Function; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) implies f is SetSequence of X )

assume that

A1: dom f = NAT and

A2: for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ; :: thesis: f is SetSequence of X

rng f c= bool X

proof

hence
f is SetSequence of X
by A1, FUNCT_2:2; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in bool X )

assume z in rng f ; :: thesis: z in bool X

then consider x being object such that

A3: x in dom f and

A4: z = f . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A1, A3;

set Y = { (B . k) where k is Nat : n <= k } ;

set y = meet { (B . k) where k is Nat : n <= k } ;

A5: meet { (B . k) where k is Nat : n <= k } is Subset of X

hence z in bool X by A5; :: thesis: verum

end;assume z in rng f ; :: thesis: z in bool X

then consider x being object such that

A3: x in dom f and

A4: z = f . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A1, A3;

set Y = { (B . k) where k is Nat : n <= k } ;

set y = meet { (B . k) where k is Nat : n <= k } ;

A5: meet { (B . k) where k is Nat : n <= k } is Subset of X

proof
end;

z = meet { (B . k) where k is Nat : n <= k }
by A2, A4;per cases
( { (B . k) where k is Nat : n <= k } <> {} or { (B . k) where k is Nat : n <= k } = {} )
;

end;

suppose
{ (B . k) where k is Nat : n <= k } <> {}
; :: thesis: meet { (B . k) where k is Nat : n <= k } is Subset of X

then consider Z1 being object such that

A6: Z1 in { (B . k) where k is Nat : n <= k } by XBOOLE_0:def 1;

reconsider Z1 = Z1 as set by TARSKI:1;

consider k1 being Nat such that

A7: ( Z1 = B . k1 & n <= k1 ) by A6;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

end;A6: Z1 in { (B . k) where k is Nat : n <= k } by XBOOLE_0:def 1;

reconsider Z1 = Z1 as set by TARSKI:1;

consider k1 being Nat such that

A7: ( Z1 = B . k1 & n <= k1 ) by A6;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

now :: thesis: for x being object st x in meet { (B . k) where k is Nat : n <= k } holds

x in X

hence
meet { (B . k) where k is Nat : n <= k } is Subset of X
by TARSKI:def 3; :: thesis: verumx in X

let x be object ; :: thesis: ( x in meet { (B . k) where k is Nat : n <= k } implies x in X )

assume x in meet { (B . k) where k is Nat : n <= k } ; :: thesis: x in X

then x in Z1 by A6, SETFAM_1:def 1;

then x in B . k1 by A7;

hence x in X ; :: thesis: verum

end;assume x in meet { (B . k) where k is Nat : n <= k } ; :: thesis: x in X

then x in Z1 by A6, SETFAM_1:def 1;

then x in B . k1 by A7;

hence x in X ; :: thesis: verum

hence z in bool X by A5; :: thesis: verum