let x be object ; :: thesis: for X being set

for B being SetSequence of X holds

( x in meet (rng B) iff for n being Nat holds x in B . n )

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

( x in meet (rng B) iff for n being Nat holds x in B . n )

let B be SetSequence of X; :: thesis: ( x in meet (rng B) iff for n being Nat holds x in B . n )

A1: dom B = NAT by FUNCT_2:def 1;

for B being SetSequence of X holds

( x in meet (rng B) iff for n being Nat holds x in B . n )

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

( x in meet (rng B) iff for n being Nat holds x in B . n )

let B be SetSequence of X; :: thesis: ( x in meet (rng B) iff for n being Nat holds x in B . n )

A1: dom B = NAT by FUNCT_2:def 1;

A2: now :: thesis: for x being object st ( for n being Nat holds x in B . n ) holds

x in meet (rng B)

x in meet (rng B)

let x be object ; :: thesis: ( ( for n being Nat holds x in B . n ) implies x in meet (rng B) )

assume A3: for n being Nat holds x in B . n ; :: thesis: x in meet (rng B)

end;assume A3: for n being Nat holds x in B . n ; :: thesis: x in meet (rng B)

now :: thesis: for Y being set st Y in rng B holds

x in Y

hence
x in meet (rng B)
by SETFAM_1:def 1; :: thesis: verumx in Y

let Y be set ; :: thesis: ( Y in rng B implies x in Y )

assume Y in rng B ; :: thesis: x in Y

then consider n being object such that

A4: n in NAT and

A5: Y = B . n by A1, FUNCT_1:def 3;

thus x in Y by A3, A4, A5; :: thesis: verum

end;assume Y in rng B ; :: thesis: x in Y

then consider n being object such that

A4: n in NAT and

A5: Y = B . n by A1, FUNCT_1:def 3;

thus x in Y by A3, A4, A5; :: thesis: verum

now :: thesis: for x being object st x in meet (rng B) holds

for n being Nat holds x in B . n

hence
( x in meet (rng B) iff for n being Nat holds x in B . n )
by A2; :: thesis: verumfor n being Nat holds x in B . n

let x be object ; :: thesis: ( x in meet (rng B) implies for n being Nat holds x in B . n )

assume A6: x in meet (rng B) ; :: thesis: for n being Nat holds x in B . n

end;assume A6: x in meet (rng B) ; :: thesis: for n being Nat holds x in B . n

now :: thesis: for k being Nat holds x in B . k

hence
for n being Nat holds x in B . n
; :: thesis: verumlet k be Nat; :: thesis: x in B . k

k in NAT by ORDINAL1:def 12;

then B . k in rng B by FUNCT_2:4;

hence x in B . k by A6, SETFAM_1:def 1; :: thesis: verum

end;k in NAT by ORDINAL1:def 12;

then B . k in rng B by FUNCT_2:4;

hence x in B . k by A6, SETFAM_1:def 1; :: thesis: verum