let X be set ; :: thesis: for SF being Subset-Family of X
for A being Element of SF holds
( id X c= block_Pervin_uniformity A & (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A )
let SF be Subset-Family of X; :: thesis: for A being Element of SF holds
( id X c= block_Pervin_uniformity A & (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A )
let A be Element of SF; :: thesis: ( id X c= block_Pervin_uniformity A & (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A )
thus id X c= block_Pervin_uniformity A :: thesis: (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in id X or t in block_Pervin_uniformity A )
assume A1: t in id X ; :: thesis: t in block_Pervin_uniformity A
then consider a, b being object such that
A2: t = [a,b] by RELAT_1:def 1;
A3: ( a in X & a = b ) by A1, A2, RELAT_1:def 10;
per cases ( a in A or not a in A ) ;
end;
end;
now :: thesis: for t being object st t in (block_Pervin_uniformity A) * (block_Pervin_uniformity A) holds
t in block_Pervin_uniformity A
let t be object ; :: thesis: ( t in (block_Pervin_uniformity A) * (block_Pervin_uniformity A) implies b1 in block_Pervin_uniformity A )
assume A4: t in (block_Pervin_uniformity A) * (block_Pervin_uniformity A) ; :: thesis: b1 in block_Pervin_uniformity A
then consider a, b being object such that
A5: t = [a,b] by RELAT_1:def 1;
[a,b] in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in block_Pervin_uniformity A & [z,y] in block_Pervin_uniformity A ) } by A5, A4, UNIFORM2:3;
then consider x, y being Element of X such that
A6: [a,b] = [x,y] and
A7: ex z being Element of X st
( [x,z] in block_Pervin_uniformity A & [z,y] in block_Pervin_uniformity A ) ;
consider z being Element of X such that
A8: [x,z] in block_Pervin_uniformity A and
A9: [z,y] in block_Pervin_uniformity A by A7;
per cases ( x in A or not x in A ) ;
suppose A10: x in A ; :: thesis: b1 in block_Pervin_uniformity A
[x,z] in [:A,A:]
proof
per cases ( [x,z] in [:(X \ A),(X \ A):] or [x,z] in [:A,A:] ) by A8, XBOOLE_0:def 3;
suppose [x,z] in [:(X \ A),(X \ A):] ; :: thesis: [x,z] in [:A,A:]
then x in X \ A by ZFMISC_1:87;
hence [x,z] in [:A,A:] by A10, XBOOLE_0:def 5; :: thesis: verum
end;
suppose [x,z] in [:A,A:] ; :: thesis: [x,z] in [:A,A:]
hence [x,z] in [:A,A:] ; :: thesis: verum
end;
end;
end;
then A11: z in A by ZFMISC_1:87;
[z,y] in [:A,A:]
proof
per cases ( [z,y] in [:(X \ A),(X \ A):] or [z,y] in [:A,A:] ) by A9, XBOOLE_0:def 3;
suppose [z,y] in [:(X \ A),(X \ A):] ; :: thesis: [z,y] in [:A,A:]
then ( z in X \ A & y in X ) by ZFMISC_1:87;
hence [z,y] in [:A,A:] by A11, XBOOLE_0:def 5; :: thesis: verum
end;
suppose [z,y] in [:A,A:] ; :: thesis: [z,y] in [:A,A:]
hence [z,y] in [:A,A:] ; :: thesis: verum
end;
end;
end;
then y in A by ZFMISC_1:87;
then [x,y] in [:A,A:] by A10, ZFMISC_1:def 2;
hence t in block_Pervin_uniformity A by A5, A6, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A12: not x in A ; :: thesis: b1 in block_Pervin_uniformity A
per cases ( X is empty or not X is empty ) ;
suppose not X is empty ; :: thesis: b1 in block_Pervin_uniformity A
then A13: x in X \ A by A12, XBOOLE_0:def 5;
[x,z] in [:(X \ A),(X \ A):]
proof
per cases ( [x,z] in [:(X \ A),(X \ A):] or [x,z] in [:A,A:] ) by A8, XBOOLE_0:def 3;
suppose [x,z] in [:(X \ A),(X \ A):] ; :: thesis: [x,z] in [:(X \ A),(X \ A):]
hence [x,z] in [:(X \ A),(X \ A):] ; :: thesis: verum
end;
suppose [x,z] in [:A,A:] ; :: thesis: [x,z] in [:(X \ A),(X \ A):]
hence [x,z] in [:(X \ A),(X \ A):] by A12, ZFMISC_1:87; :: thesis: verum
end;
end;
end;
then A14: z in X \ A by ZFMISC_1:87;
[z,y] in [:(X \ A),(X \ A):]
proof
per cases ( [z,y] in [:(X \ A),(X \ A):] or [z,y] in [:A,A:] ) by A9, XBOOLE_0:def 3;
suppose [z,y] in [:(X \ A),(X \ A):] ; :: thesis: [z,y] in [:(X \ A),(X \ A):]
hence [z,y] in [:(X \ A),(X \ A):] ; :: thesis: verum
end;
suppose [z,y] in [:A,A:] ; :: thesis: [z,y] in [:(X \ A),(X \ A):]
then ( z in A & y in A ) by ZFMISC_1:87;
hence [z,y] in [:(X \ A),(X \ A):] by A14, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
then y in X \ A by ZFMISC_1:87;
then [x,y] in [:(X \ A),(X \ A):] by A13, ZFMISC_1:def 2;
hence t in block_Pervin_uniformity A by A5, A6, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
end;
end;
hence (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A ; :: thesis: verum