let V be Universe; :: thesis: for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
( A \/ B in X & A \ B in X & A (#) B in X )
let X be Subclass of V; :: thesis: for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
( A \/ B in X & A \ B in X & A (#) B in X )
let A, B be set ; :: thesis: ( X is closed_wrt_A1-A7 & A in X & B in X implies ( A \/ B in X & A \ B in X & A (#) B in X ) )
assume that
A1: X is closed_wrt_A1-A7 and
A2: A in X and
A3: B in X ; :: thesis: ( A \/ B in X & A \ B in X & A (#) B in X )
reconsider b = B as Element of V by A3;
reconsider a = A as Element of V by A2;
A4: ( {a} in X & {b} in X ) by A1, A2, A3, Th2;
set D = { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
A5: now :: thesis: for o being object holds
( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b )
let o be object ; :: thesis: ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b )
A6: now :: thesis: ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } implies o = a \/ b )
assume o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; :: thesis: o = a \/ b
then consider x, y being Element of V such that
A7: o = x \/ y and
A8: x in {a} and
A9: y in {b} ;
x = a by A8, TARSKI:def 1;
hence o = a \/ b by A7, A9, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: ( o = a \/ b implies o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } )
A10: ( a in {a} & b in {b} ) by TARSKI:def 1;
assume o = a \/ b ; :: thesis: o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) }
hence o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A10; :: thesis: verum
end;
hence ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b ) by A6; :: thesis: verum
end;
X is closed_wrt_A5 by A1;
then { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A4;
then {(a \/ b)} in X by A5, TARSKI:def 1;
hence A \/ B in X by A1, Th2; :: thesis: ( A \ B in X & A (#) B in X )
set D = { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
A11: now :: thesis: for o being object holds
( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b )
let o be object ; :: thesis: ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b )
A12: now :: thesis: ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } implies o = a \ b )
assume o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; :: thesis: o = a \ b
then consider x, y being Element of V such that
A13: o = x \ y and
A14: x in {a} and
A15: y in {b} ;
x = a by A14, TARSKI:def 1;
hence o = a \ b by A13, A15, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: ( o = a \ b implies o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } )
A16: ( a in {a} & b in {b} ) by TARSKI:def 1;
assume o = a \ b ; :: thesis: o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) }
hence o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A16; :: thesis: verum
end;
hence ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b ) by A12; :: thesis: verum
end;
X is closed_wrt_A6 by A1;
then { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A4;
then {(a \ b)} in X by A11, TARSKI:def 1;
hence A \ B in X by A1, Th2; :: thesis: A (#) B in X
set D = { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
A17: now :: thesis: for o being object holds
( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b )
let o be object ; :: thesis: ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b )
A18: now :: thesis: ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } implies o = a (#) b )
assume o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; :: thesis: o = a (#) b
then consider x, y being Element of V such that
A19: o = x (#) y and
A20: x in {a} and
A21: y in {b} ;
x = a by A20, TARSKI:def 1;
hence o = a (#) b by A19, A21, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: ( o = a (#) b implies o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } )
A22: ( a in {a} & b in {b} ) by TARSKI:def 1;
assume o = a (#) b ; :: thesis: o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) }
hence o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A22; :: thesis: verum
end;
hence ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b ) by A18; :: thesis: verum
end;
X is closed_wrt_A7 by A1;
then { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A4;
then {(a (#) b)} in X by A17, TARSKI:def 1;
hence A (#) B in X by A1, Th2; :: thesis: verum