:: DOMAIN_1 semantic presentation begin theorem :: DOMAIN_1:1 for a being set for X1, X2 being non empty set st a in [:X1,X2:] holds ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2] proof let a be set ; ::_thesis: for X1, X2 being non empty set st a in [:X1,X2:] holds ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2] let X1, X2 be non empty set ; ::_thesis: ( a in [:X1,X2:] implies ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2] ) assume a in [:X1,X2:] ; ::_thesis: ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2] then consider x1, x2 being set such that A1: x1 in X1 and A2: x2 in X2 and A3: a = [x1,x2] by ZFMISC_1:def_2; reconsider x2 = x2 as Element of X2 by A2; reconsider x1 = x1 as Element of X1 by A1; take x1 ; ::_thesis: ex x2 being Element of X2 st a = [x1,x2] take x2 ; ::_thesis: a = [x1,x2] thus a = [x1,x2] by A3; ::_thesis: verum end; theorem :: DOMAIN_1:2 for X1, X2 being non empty set for x, y being Element of [:X1,X2:] st x `1 = y `1 & x `2 = y `2 holds x = y proof let X1, X2 be non empty set ; ::_thesis: for x, y being Element of [:X1,X2:] st x `1 = y `1 & x `2 = y `2 holds x = y let x, y be Element of [:X1,X2:]; ::_thesis: ( x `1 = y `1 & x `2 = y `2 implies x = y ) [(x `1),(x `2)] = x by MCART_1:21; hence ( x `1 = y `1 & x `2 = y `2 implies x = y ) by MCART_1:21; ::_thesis: verum end; definition let X1, X2 be non empty set ; let x1 be Element of X1; let x2 be Element of X2; :: original: [ redefine func[x1,x2] -> Element of [:X1,X2:]; coherence [x1,x2] is Element of [:X1,X2:] by ZFMISC_1:87; end; definition let X1, X2 be non empty set ; let x be Element of [:X1,X2:]; :: original: `1 redefine funcx `1 -> Element of X1; coherence x `1 is Element of X1 by MCART_1:10; :: original: `2 redefine funcx `2 -> Element of X2; coherence x `2 is Element of X2 by MCART_1:10; end; theorem Th3: :: DOMAIN_1:3 for a being set for X1, X2, X3 being non empty set holds ( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) proof let a be set ; ::_thesis: for X1, X2, X3 being non empty set holds ( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) let X1, X2, X3 be non empty set ; ::_thesis: ( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) thus ( a in [:X1,X2,X3:] implies ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ::_thesis: ( ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] implies a in [:X1,X2,X3:] ) proof assume a in [:X1,X2,X3:] ; ::_thesis: ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] then a in [:[:X1,X2:],X3:] by ZFMISC_1:def_3; then consider x12, x3 being set such that A1: x12 in [:X1,X2:] and A2: x3 in X3 and A3: a = [x12,x3] by ZFMISC_1:def_2; reconsider x3 = x3 as Element of X3 by A2; consider x1, x2 being set such that A4: x1 in X1 and A5: x2 in X2 and A6: x12 = [x1,x2] by A1, ZFMISC_1:def_2; reconsider x2 = x2 as Element of X2 by A5; reconsider x1 = x1 as Element of X1 by A4; a = [x1,x2,x3] by A3, A6; hence ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ; ::_thesis: verum end; given x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that A7: a = [x1,x2,x3] ; ::_thesis: a in [:X1,X2,X3:] a = [[x1,x2],x3] by A7; then a in [:[:X1,X2:],X3:] ; hence a in [:X1,X2,X3:] by ZFMISC_1:def_3; ::_thesis: verum end; theorem Th4: :: DOMAIN_1:4 for D, X1, X2, X3 being non empty set st ( for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) holds D = [:X1,X2,X3:] proof let D, X1, X2, X3 be non empty set ; ::_thesis: ( ( for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) implies D = [:X1,X2,X3:] ) assume A1: for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ; ::_thesis: D = [:X1,X2,X3:] now__::_thesis:_for_a_being_set_holds_ (_(_a_in_D_implies_a_in_[:[:X1,X2:],X3:]_)_&_(_a_in_[:[:X1,X2:],X3:]_implies_a_in_D_)_) let a be set ; ::_thesis: ( ( a in D implies a in [:[:X1,X2:],X3:] ) & ( a in [:[:X1,X2:],X3:] implies a in D ) ) thus ( a in D implies a in [:[:X1,X2:],X3:] ) ::_thesis: ( a in [:[:X1,X2:],X3:] implies a in D ) proof assume a in D ; ::_thesis: a in [:[:X1,X2:],X3:] then consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that A2: a = [x1,x2,x3] by A1; a = [[x1,x2],x3] by A2; hence a in [:[:X1,X2:],X3:] ; ::_thesis: verum end; assume a in [:[:X1,X2:],X3:] ; ::_thesis: a in D then consider x12, x3 being set such that A3: x12 in [:X1,X2:] and A4: x3 in X3 and A5: a = [x12,x3] by ZFMISC_1:def_2; reconsider x3 = x3 as Element of X3 by A4; consider x1, x2 being set such that A6: x1 in X1 and A7: x2 in X2 and A8: x12 = [x1,x2] by A3, ZFMISC_1:def_2; reconsider x2 = x2 as Element of X2 by A7; reconsider x1 = x1 as Element of X1 by A6; a = [x1,x2,x3] by A5, A8; hence a in D by A1; ::_thesis: verum end; then D = [:[:X1,X2:],X3:] by TARSKI:1; hence D = [:X1,X2,X3:] by ZFMISC_1:def_3; ::_thesis: verum end; theorem :: DOMAIN_1:5 for D, X1, X2, X3 being non empty set holds ( D = [:X1,X2,X3:] iff for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) by Th3, Th4; definition let X1, X2, X3 be non empty set ; let x1 be Element of X1; let x2 be Element of X2; let x3 be Element of X3; :: original: [ redefine func[x1,x2,x3] -> Element of [:X1,X2,X3:]; coherence [x1,x2,x3] is Element of [:X1,X2,X3:] by MCART_1:69; end; theorem :: DOMAIN_1:6 for a being set for X1, X2, X3 being non empty set for x being Element of [:X1,X2,X3:] holds ( a = x `1_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) proof let a be set ; ::_thesis: for X1, X2, X3 being non empty set for x being Element of [:X1,X2,X3:] holds ( a = x `1_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds ( a = x `1_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) let x be Element of [:X1,X2,X3:]; ::_thesis: ( a = x `1_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) thus ( a = x `1_3 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) implies a = x `1_3 ) proof A1: x = [(x `1_3),(x `2_3),(x `3_3)] ; assume A2: a = x `1_3 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 let x3 be Element of X3; ::_thesis: ( x = [x1,x2,x3] implies a = x1 ) assume x = [x1,x2,x3] ; ::_thesis: a = x1 hence a = x1 by A2, A1, XTUPLE_0:3; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds a = x1 ) implies a = x `1_3 ) by MCART_1:65; ::_thesis: verum end; theorem :: DOMAIN_1:7 for b being set for X1, X2, X3 being non empty set for x being Element of [:X1,X2,X3:] holds ( b = x `2_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) proof let b be set ; ::_thesis: for X1, X2, X3 being non empty set for x being Element of [:X1,X2,X3:] holds ( b = x `2_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds ( b = x `2_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) let x be Element of [:X1,X2,X3:]; ::_thesis: ( b = x `2_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) thus ( b = x `2_3 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) implies b = x `2_3 ) proof A1: x = [(x `1_3),(x `2_3),(x `3_3)] ; assume A2: b = x `2_3 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 let x3 be Element of X3; ::_thesis: ( x = [x1,x2,x3] implies b = x2 ) assume x = [x1,x2,x3] ; ::_thesis: b = x2 hence b = x2 by A2, A1, XTUPLE_0:3; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds b = x2 ) implies b = x `2_3 ) by MCART_1:66; ::_thesis: verum end; theorem :: DOMAIN_1:8 for c being set for X1, X2, X3 being non empty set for x being Element of [:X1,X2,X3:] holds ( c = x `3_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) proof let c be set ; ::_thesis: for X1, X2, X3 being non empty set for x being Element of [:X1,X2,X3:] holds ( c = x `3_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds ( c = x `3_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) let x be Element of [:X1,X2,X3:]; ::_thesis: ( c = x `3_3 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) thus ( c = x `3_3 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) implies c = x `3_3 ) proof A1: x = [(x `1_3),(x `2_3),(x `3_3)] ; assume A2: c = x `3_3 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 let x3 be Element of X3; ::_thesis: ( x = [x1,x2,x3] implies c = x3 ) assume x = [x1,x2,x3] ; ::_thesis: c = x3 hence c = x3 by A2, A1, XTUPLE_0:3; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 st x = [x1,x2,x3] holds c = x3 ) implies c = x `3_3 ) by MCART_1:67; ::_thesis: verum end; theorem :: DOMAIN_1:9 for X1, X2, X3 being non empty set for x, y being Element of [:X1,X2,X3:] st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 holds x = y proof let X1, X2, X3 be non empty set ; ::_thesis: for x, y being Element of [:X1,X2,X3:] st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 holds x = y let x, y be Element of [:X1,X2,X3:]; ::_thesis: ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 implies x = y ) [(x `1_3),(x `2_3),(x `3_3)] = x ; hence ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 implies x = y ) by MCART_1:44; ::_thesis: verum end; theorem Th10: :: DOMAIN_1:10 for a being set for X1, X2, X3, X4 being non empty set holds ( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) proof let a be set ; ::_thesis: for X1, X2, X3, X4 being non empty set holds ( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) let X1, X2, X3, X4 be non empty set ; ::_thesis: ( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) thus ( a in [:X1,X2,X3,X4:] implies ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ::_thesis: ( ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] implies a in [:X1,X2,X3,X4:] ) proof assume a in [:X1,X2,X3,X4:] ; ::_thesis: ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] then a in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def_4; then consider x123, x4 being set such that A1: x123 in [:X1,X2,X3:] and A2: x4 in X4 and A3: a = [x123,x4] by ZFMISC_1:def_2; reconsider x4 = x4 as Element of X4 by A2; consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that A4: x123 = [x1,x2,x3] by A1, Th3; a = [x1,x2,x3,x4] by A3, A4; hence ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ; ::_thesis: verum end; given x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that A5: a = [x1,x2,x3,x4] ; ::_thesis: a in [:X1,X2,X3,X4:] a = [[x1,x2,x3],x4] by A5; then a in [:[:X1,X2,X3:],X4:] ; hence a in [:X1,X2,X3,X4:] by ZFMISC_1:def_4; ::_thesis: verum end; theorem Th11: :: DOMAIN_1:11 for D, X1, X2, X3, X4 being non empty set st ( for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) holds D = [:X1,X2,X3,X4:] proof let D, X1, X2, X3, X4 be non empty set ; ::_thesis: ( ( for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) implies D = [:X1,X2,X3,X4:] ) assume A1: for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ; ::_thesis: D = [:X1,X2,X3,X4:] now__::_thesis:_for_a_being_set_holds_ (_(_a_in_D_implies_a_in_[:[:X1,X2,X3:],X4:]_)_&_(_a_in_[:[:X1,X2,X3:],X4:]_implies_a_in_D_)_) let a be set ; ::_thesis: ( ( a in D implies a in [:[:X1,X2,X3:],X4:] ) & ( a in [:[:X1,X2,X3:],X4:] implies a in D ) ) thus ( a in D implies a in [:[:X1,X2,X3:],X4:] ) ::_thesis: ( a in [:[:X1,X2,X3:],X4:] implies a in D ) proof assume a in D ; ::_thesis: a in [:[:X1,X2,X3:],X4:] then consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that A2: a = [x1,x2,x3,x4] by A1; a = [[x1,x2,x3],x4] by A2; hence a in [:[:X1,X2,X3:],X4:] ; ::_thesis: verum end; assume a in [:[:X1,X2,X3:],X4:] ; ::_thesis: a in D then consider x123, x4 being set such that A3: x123 in [:X1,X2,X3:] and A4: x4 in X4 and A5: a = [x123,x4] by ZFMISC_1:def_2; reconsider x4 = x4 as Element of X4 by A4; consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that A6: x123 = [x1,x2,x3] by A3, Th3; a = [x1,x2,x3,x4] by A5, A6; hence a in D by A1; ::_thesis: verum end; then D = [:[:X1,X2,X3:],X4:] by TARSKI:1; hence D = [:X1,X2,X3,X4:] by ZFMISC_1:def_4; ::_thesis: verum end; theorem :: DOMAIN_1:12 for D, X1, X2, X3, X4 being non empty set holds ( D = [:X1,X2,X3,X4:] iff for a being set holds ( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) by Th10, Th11; definition let X1, X2, X3, X4 be non empty set ; let x1 be Element of X1; let x2 be Element of X2; let x3 be Element of X3; let x4 be Element of X4; :: original: [ redefine func[x1,x2,x3,x4] -> Element of [:X1,X2,X3,X4:]; coherence [x1,x2,x3,x4] is Element of [:X1,X2,X3,X4:] by MCART_1:80; end; theorem :: DOMAIN_1:13 for a being set for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( a = x `1_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) proof let a be set ; ::_thesis: for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( a = x `1_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds ( a = x `1_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( a = x `1_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) thus ( a = x `1_4 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) implies a = x `1_4 ) proof A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ; assume A2: a = x `1_4 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies a = x1 ) assume x = [x1,x2,x3,x4] ; ::_thesis: a = x1 hence a = x1 by A2, A1, XTUPLE_0:5; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds a = x1 ) implies a = x `1_4 ) by MCART_1:75; ::_thesis: verum end; theorem :: DOMAIN_1:14 for b being set for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( b = x `2_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) proof let b be set ; ::_thesis: for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( b = x `2_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds ( b = x `2_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( b = x `2_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) thus ( b = x `2_4 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) implies b = x `2_4 ) proof A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ; assume A2: b = x `2_4 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies b = x2 ) assume x = [x1,x2,x3,x4] ; ::_thesis: b = x2 hence b = x2 by A2, A1, XTUPLE_0:5; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds b = x2 ) implies b = x `2_4 ) by MCART_1:76; ::_thesis: verum end; theorem :: DOMAIN_1:15 for c being set for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( c = x `3_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) proof let c be set ; ::_thesis: for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( c = x `3_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds ( c = x `3_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( c = x `3_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) thus ( c = x `3_4 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) implies c = x `3_4 ) proof A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ; assume A2: c = x `3_4 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies c = x3 ) assume x = [x1,x2,x3,x4] ; ::_thesis: c = x3 hence c = x3 by A2, A1, XTUPLE_0:5; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds c = x3 ) implies c = x `3_4 ) by MCART_1:77; ::_thesis: verum end; theorem :: DOMAIN_1:16 for d being set for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( d = x `4_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) proof let d be set ; ::_thesis: for X1, X2, X3, X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds ( d = x `4_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds ( d = x `4_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( d = x `4_4 iff for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) thus ( d = x `4_4 implies for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) ::_thesis: ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) implies d = x `4_4 ) proof A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ; assume A2: d = x `4_4 ; ::_thesis: for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 let x1 be Element of X1; ::_thesis: for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 let x2 be Element of X2; ::_thesis: for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies d = x4 ) assume x = [x1,x2,x3,x4] ; ::_thesis: d = x4 hence d = x4 by A2, A1, XTUPLE_0:5; ::_thesis: verum end; thus ( ( for x1 being Element of X1 for x2 being Element of X2 for x3 being Element of X3 for x4 being Element of X4 st x = [x1,x2,x3,x4] holds d = x4 ) implies d = x `4_4 ) by MCART_1:78; ::_thesis: verum end; theorem :: DOMAIN_1:17 for X1, X2, X3, X4 being non empty set for x, y being Element of [:X1,X2,X3,X4:] st x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 holds x = y proof let X1, X2, X3, X4 be non empty set ; ::_thesis: for x, y being Element of [:X1,X2,X3,X4:] st x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 holds x = y let x, y be Element of [:X1,X2,X3,X4:]; ::_thesis: ( x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 implies x = y ) [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] = x ; hence ( x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 implies x = y ) by MCART_1:56; ::_thesis: verum end; scheme :: DOMAIN_1:sch 1 Fraenkel1{ P1[ set ] } : for X1 being non empty set holds { x1 where x1 is Element of X1 : P1[x1] } is Subset of X1 proof let X1 be non empty set ; ::_thesis: { x1 where x1 is Element of X1 : P1[x1] } is Subset of X1 { x1 where x1 is Element of X1 : P1[x1] } c= X1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : P1[x1] } or a in X1 ) assume a in { x1 where x1 is Element of X1 : P1[x1] } ; ::_thesis: a in X1 then ex x1 being Element of X1 st ( a = x1 & P1[x1] ) ; hence a in X1 ; ::_thesis: verum end; hence { x1 where x1 is Element of X1 : P1[x1] } is Subset of X1 ; ::_thesis: verum end; scheme :: DOMAIN_1:sch 2 Fraenkel2{ P1[ set , set ] } : for X1, X2 being non empty set holds { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2] } is Subset of [:X1,X2:] proof let X1, X2 be non empty set ; ::_thesis: { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2] } is Subset of [:X1,X2:] { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2] } c= [:X1,X2:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2] } or a in [:X1,X2:] ) assume a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2] } ; ::_thesis: a in [:X1,X2:] then ex x1 being Element of X1 ex x2 being Element of X2 st ( a = [x1,x2] & P1[x1,x2] ) ; hence a in [:X1,X2:] ; ::_thesis: verum end; hence { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2] } is Subset of [:X1,X2:] ; ::_thesis: verum end; scheme :: DOMAIN_1:sch 3 Fraenkel3{ P1[ set , set , set ] } : for X1, X2, X3 being non empty set holds { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } is Subset of [:X1,X2,X3:] proof let X1, X2, X3 be non empty set ; ::_thesis: { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } is Subset of [:X1,X2,X3:] { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } c= [:X1,X2,X3:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } or a in [:X1,X2,X3:] ) assume a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } ; ::_thesis: a in [:X1,X2,X3:] then ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st ( a = [x1,x2,x3] & P1[x1,x2,x3] ) ; hence a in [:X1,X2,X3:] ; ::_thesis: verum end; hence { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } is Subset of [:X1,X2,X3:] ; ::_thesis: verum end; scheme :: DOMAIN_1:sch 4 Fraenkel4{ P1[ set , set , set , set ] } : for X1, X2, X3, X4 being non empty set holds { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:] proof let X1, X2, X3, X4 be non empty set ; ::_thesis: { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:] { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } c= [:X1,X2,X3,X4:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } or a in [:X1,X2,X3,X4:] ) assume a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } ; ::_thesis: a in [:X1,X2,X3,X4:] then ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st ( a = [x1,x2,x3,x4] & P1[x1,x2,x3,x4] ) ; hence a in [:X1,X2,X3,X4:] ; ::_thesis: verum end; hence { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:] ; ::_thesis: verum end; scheme :: DOMAIN_1:sch 5 Fraenkel5{ P1[ set ], P2[ set ] } : for X1 being non empty set st ( for x1 being Element of X1 st P1[x1] holds P2[x1] ) holds { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } proof let X1 be non empty set ; ::_thesis: ( ( for x1 being Element of X1 st P1[x1] holds P2[x1] ) implies { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } ) assume A1: for x1 being Element of X1 st P1[x1] holds P2[x1] ; ::_thesis: { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { y1 where y1 is Element of X1 : P1[y1] } or a in { z1 where z1 is Element of X1 : P2[z1] } ) assume a in { x1 where x1 is Element of X1 : P1[x1] } ; ::_thesis: a in { z1 where z1 is Element of X1 : P2[z1] } then consider x1 being Element of X1 such that A2: a = x1 and A3: P1[x1] ; P2[x1] by A1, A3; hence a in { z1 where z1 is Element of X1 : P2[z1] } by A2; ::_thesis: verum end; scheme :: DOMAIN_1:sch 6 Fraenkel6{ P1[ set ], P2[ set ] } : for X1 being non empty set st ( for x1 being Element of X1 holds ( P1[x1] iff P2[x1] ) ) holds { y1 where y1 is Element of X1 : P1[y1] } = { z1 where z1 is Element of X1 : P2[z1] } proof let X1 be non empty set ; ::_thesis: ( ( for x1 being Element of X1 holds ( P1[x1] iff P2[x1] ) ) implies { y1 where y1 is Element of X1 : P1[y1] } = { z1 where z1 is Element of X1 : P2[z1] } ) assume A1: for x1 being Element of X1 holds ( P1[x1] iff P2[x1] ) ; ::_thesis: { y1 where y1 is Element of X1 : P1[y1] } = { z1 where z1 is Element of X1 : P2[z1] } for X1 being non empty set st ( for x1 being Element of X1 st P1[x1] holds P2[x1] ) holds { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } from DOMAIN_1:sch_5(); hence { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } by A1; :: according to XBOOLE_0:def_10 ::_thesis: { z1 where z1 is Element of X1 : P2[z1] } c= { y1 where y1 is Element of X1 : P1[y1] } for X1 being non empty set st ( for x1 being Element of X1 st P2[x1] holds P1[x1] ) holds { y1 where y1 is Element of X1 : P2[y1] } c= { z1 where z1 is Element of X1 : P1[z1] } from DOMAIN_1:sch_5(); hence { z1 where z1 is Element of X1 : P2[z1] } c= { y1 where y1 is Element of X1 : P1[y1] } by A1; ::_thesis: verum end; scheme :: DOMAIN_1:sch 7 SubsetD{ F1() -> non empty set , P1[ set ] } : { d where d is Element of F1() : P1[d] } is Subset of F1() proof for D being non empty set holds { d where d is Element of D : P1[d] } is Subset of D from DOMAIN_1:sch_1(); hence { d where d is Element of F1() : P1[d] } is Subset of F1() ; ::_thesis: verum end; theorem :: DOMAIN_1:18 for X1 being non empty set holds X1 = { x1 where x1 is Element of X1 : verum } proof let X1 be non empty set ; ::_thesis: X1 = { x1 where x1 is Element of X1 : verum } defpred S1[ set ] means verum; A1: for y1 being Element of X1 holds y1 in { x1 where x1 is Element of X1 : verum } ; { x1 where x1 is Element of X1 : S1[x1] } is Subset of X1 from DOMAIN_1:sch_7(); hence X1 = { x1 where x1 is Element of X1 : verum } by A1, SUBSET_1:28; ::_thesis: verum end; theorem :: DOMAIN_1:19 for X1, X2 being non empty set holds [:X1,X2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } proof let X1, X2 be non empty set ; ::_thesis: [:X1,X2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } defpred S1[ set , set ] means verum; A1: for x being Element of [:X1,X2:] holds x in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } proof let x be Element of [:X1,X2:]; ::_thesis: x in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } x = [(x `1),(x `2)] by MCART_1:21; hence x in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } ; ::_thesis: verum end; for X1, X2 being non empty set holds { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : S1[x1,x2] } is Subset of [:X1,X2:] from DOMAIN_1:sch_2(); then { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } is Subset of [:X1,X2:] ; hence [:X1,X2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum } by A1, SUBSET_1:28; ::_thesis: verum end; theorem :: DOMAIN_1:20 for X1, X2, X3 being non empty set holds [:X1,X2,X3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } proof let X1, X2, X3 be non empty set ; ::_thesis: [:X1,X2,X3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } defpred S1[ set , set , set ] means verum; A1: for x being Element of [:X1,X2,X3:] holds x in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } proof let x be Element of [:X1,X2,X3:]; ::_thesis: x in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } x = [(x `1_3),(x `2_3),(x `3_3)] ; hence x in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } ; ::_thesis: verum end; for X1, X2, X3 being non empty set holds { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : S1[x1,x2,x3] } is Subset of [:X1,X2,X3:] from DOMAIN_1:sch_3(); then { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } is Subset of [:X1,X2,X3:] ; hence [:X1,X2,X3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } by A1, SUBSET_1:28; ::_thesis: verum end; theorem :: DOMAIN_1:21 for X1, X2, X3, X4 being non empty set holds [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } proof let X1, X2, X3, X4 be non empty set ; ::_thesis: [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } defpred S1[ set , set , set , set ] means verum; A1: for x being Element of [:X1,X2,X3,X4:] holds x in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } proof let x be Element of [:X1,X2,X3,X4:]; ::_thesis: x in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ; hence x in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } ; ::_thesis: verum end; for X1, X2, X3, X4 being non empty set holds { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : S1[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:] from DOMAIN_1:sch_4(); then { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } is Subset of [:X1,X2,X3,X4:] ; hence [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } by A1, SUBSET_1:28; ::_thesis: verum end; theorem :: DOMAIN_1:22 for X1 being non empty set for A1 being Subset of X1 holds A1 = { x1 where x1 is Element of X1 : x1 in A1 } proof let X1 be non empty set ; ::_thesis: for A1 being Subset of X1 holds A1 = { x1 where x1 is Element of X1 : x1 in A1 } let A1 be Subset of X1; ::_thesis: A1 = { x1 where x1 is Element of X1 : x1 in A1 } thus A1 c= { x1 where x1 is Element of X1 : x1 in A1 } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : x1 in A1 } c= A1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in { x1 where x1 is Element of X1 : x1 in A1 } ) assume a in A1 ; ::_thesis: a in { x1 where x1 is Element of X1 : x1 in A1 } hence a in { x1 where x1 is Element of X1 : x1 in A1 } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : x1 in A1 } or a in A1 ) assume a in { x1 where x1 is Element of X1 : x1 in A1 } ; ::_thesis: a in A1 then ex x1 being Element of X1 st ( a = x1 & x1 in A1 ) ; hence a in A1 ; ::_thesis: verum end; theorem :: DOMAIN_1:23 for X1, X2 being non empty set for A1 being Subset of X1 for A2 being Subset of X2 holds [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } proof let X1, X2 be non empty set ; ::_thesis: for A1 being Subset of X1 for A2 being Subset of X2 holds [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } let A1 be Subset of X1; ::_thesis: for A2 being Subset of X2 holds [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } let A2 be Subset of X2; ::_thesis: [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } thus [:A1,A2:] c= { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } c= [:A1,A2:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:A1,A2:] or a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } ) assume A1: a in [:A1,A2:] ; ::_thesis: a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } then reconsider x = a as Element of [:X1,X2:] ; A2: x = [(x `1),(x `2)] by MCART_1:21; ( x `1 in A1 & x `2 in A2 ) by A1, MCART_1:10; hence a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } by A2; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } or a in [:A1,A2:] ) assume a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } ; ::_thesis: a in [:A1,A2:] then ex x1 being Element of X1 ex x2 being Element of X2 st ( a = [x1,x2] & x1 in A1 & x2 in A2 ) ; hence a in [:A1,A2:] by ZFMISC_1:87; ::_thesis: verum end; theorem :: DOMAIN_1:24 for X1, X2, X3 being non empty set for A1 being Subset of X1 for A2 being Subset of X2 for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } proof let X1, X2, X3 be non empty set ; ::_thesis: for A1 being Subset of X1 for A2 being Subset of X2 for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } let A1 be Subset of X1; ::_thesis: for A2 being Subset of X2 for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } let A2 be Subset of X2; ::_thesis: for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } let A3 be Subset of X3; ::_thesis: [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } thus [:A1,A2,A3:] c= { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } :: according to XBOOLE_0:def_10 ::_thesis: { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } c= [:A1,A2,A3:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:A1,A2,A3:] or a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } ) assume B1: a in [:A1,A2,A3:] ; ::_thesis: a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } reconsider A1 = A1 as non empty Subset of X1 by B1, MCART_1:31; reconsider A2 = A2 as non empty Subset of X2 by B1, MCART_1:31; reconsider A3 = A3 as non empty Subset of X3 by B1, MCART_1:31; A1: a in [:A1,A2,A3:] by B1; reconsider x = a as Element of [:X1,X2,X3:] by A1; B2: x = [(x `1_3),(x `2_3),(x `3_3)] ; A2: x `3_3 in A3 by A1, MCART_1:72; ( x `1_3 in A1 & x `2_3 in A2 ) by A1, MCART_1:72; hence a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } by A2, B2; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } or a in [:A1,A2,A3:] ) assume a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } ; ::_thesis: a in [:A1,A2,A3:] then ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st ( a = [x1,x2,x3] & x1 in A1 & x2 in A2 & x3 in A3 ) ; hence a in [:A1,A2,A3:] by MCART_1:69; ::_thesis: verum end; theorem :: DOMAIN_1:25 for X1, X2, X3, X4 being non empty set for A1 being Subset of X1 for A2 being Subset of X2 for A3 being Subset of X3 for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } proof let X1, X2, X3, X4 be non empty set ; ::_thesis: for A1 being Subset of X1 for A2 being Subset of X2 for A3 being Subset of X3 for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } let A1 be Subset of X1; ::_thesis: for A2 being Subset of X2 for A3 being Subset of X3 for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } let A2 be Subset of X2; ::_thesis: for A3 being Subset of X3 for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } let A3 be Subset of X3; ::_thesis: for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } let A4 be Subset of X4; ::_thesis: [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } thus [:A1,A2,A3,A4:] c= { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } :: according to XBOOLE_0:def_10 ::_thesis: { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } c= [:A1,A2,A3,A4:] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:A1,A2,A3,A4:] or a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } ) assume B1: a in [:A1,A2,A3,A4:] ; ::_thesis: a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } reconsider A1 = A1 as non empty Subset of X1 by B1, MCART_1:51; reconsider A2 = A2 as non empty Subset of X2 by B1, MCART_1:51; reconsider A3 = A3 as non empty Subset of X3 by B1, MCART_1:51; reconsider A4 = A4 as non empty Subset of X4 by B1, MCART_1:51; A1: a in [:A1,A2,A3,A4:] by B1; then reconsider x = a as Element of [:X1,X2,X3,X4:] ; A2: ( x `3_4 in A3 & x `4_4 in A4 ) by A1, MCART_1:83; A3: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ; ( x `1_4 in A1 & x `2_4 in A2 ) by A1, MCART_1:83; hence a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } by A3, A2; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } or a in [:A1,A2,A3,A4:] ) assume a in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } ; ::_thesis: a in [:A1,A2,A3,A4:] then ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st ( a = [x1,x2,x3,x4] & x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) ; hence a in [:A1,A2,A3,A4:] by MCART_1:80; ::_thesis: verum end; theorem :: DOMAIN_1:26 for X1 being non empty set holds {} X1 = { x1 where x1 is Element of X1 : contradiction } proof let X1 be non empty set ; ::_thesis: {} X1 = { x1 where x1 is Element of X1 : contradiction } thus {} X1 c= { x1 where x1 is Element of X1 : contradiction } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : contradiction } c= {} X1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {} X1 or a in { x1 where x1 is Element of X1 : contradiction } ) thus ( not a in {} X1 or a in { x1 where x1 is Element of X1 : contradiction } ) ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : contradiction } or a in {} X1 ) assume a in { x1 where x1 is Element of X1 : contradiction } ; ::_thesis: a in {} X1 then ex x1 being Element of X1 st ( a = x1 & contradiction ) ; hence a in {} X1 ; ::_thesis: verum end; theorem :: DOMAIN_1:27 for X1 being non empty set for A1 being Subset of X1 holds A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 } proof let X1 be non empty set ; ::_thesis: for A1 being Subset of X1 holds A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 } let A1 be Subset of X1; ::_thesis: A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 } thus A1 ` c= { x1 where x1 is Element of X1 : not x1 in A1 } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : not x1 in A1 } c= A1 ` proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 ` or a in { x1 where x1 is Element of X1 : not x1 in A1 } ) assume A1: a in A1 ` ; ::_thesis: a in { x1 where x1 is Element of X1 : not x1 in A1 } then not a in A1 by XBOOLE_0:def_5; hence a in { x1 where x1 is Element of X1 : not x1 in A1 } by A1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : not x1 in A1 } or a in A1 ` ) assume a in { x1 where x1 is Element of X1 : not x1 in A1 } ; ::_thesis: a in A1 ` then ex x1 being Element of X1 st ( a = x1 & not x1 in A1 ) ; hence a in A1 ` by SUBSET_1:29; ::_thesis: verum end; theorem :: DOMAIN_1:28 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 /\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 /\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } let A1, B1 be Subset of X1; ::_thesis: A1 /\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } thus A1 /\ B1 c= { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } c= A1 /\ B1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 /\ B1 or a in { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } ) assume A1: a in A1 /\ B1 ; ::_thesis: a in { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } then reconsider x = a as Element of X1 ; ( x in A1 & x in B1 ) by A1, XBOOLE_0:def_4; hence a in { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } or a in A1 /\ B1 ) assume a in { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) } ; ::_thesis: a in A1 /\ B1 then ex x1 being Element of X1 st ( a = x1 & x1 in A1 & x1 in B1 ) ; hence a in A1 /\ B1 by XBOOLE_0:def_4; ::_thesis: verum end; theorem :: DOMAIN_1:29 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 \/ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \/ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } let A1, B1 be Subset of X1; ::_thesis: A1 \/ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } thus A1 \/ B1 c= { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } c= A1 \/ B1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 \/ B1 or a in { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } ) assume A1: a in A1 \/ B1 ; ::_thesis: a in { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } then reconsider x = a as Element of X1 ; ( x in A1 or x in B1 ) by A1, XBOOLE_0:def_3; hence a in { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } or a in A1 \/ B1 ) assume a in { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) } ; ::_thesis: a in A1 \/ B1 then ex x1 being Element of X1 st ( a = x1 & ( x1 in A1 or x1 in B1 ) ) ; hence a in A1 \/ B1 by XBOOLE_0:def_3; ::_thesis: verum end; theorem :: DOMAIN_1:30 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 \ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } let A1, B1 be Subset of X1; ::_thesis: A1 \ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } thus A1 \ B1 c= { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } c= A1 \ B1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 \ B1 or a in { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } ) assume A1: a in A1 \ B1 ; ::_thesis: a in { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } then reconsider x = a as Element of X1 ; ( x in A1 & not x in B1 ) by A1, XBOOLE_0:def_5; hence a in { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } or a in A1 \ B1 ) assume a in { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) } ; ::_thesis: a in A1 \ B1 then ex x1 being Element of X1 st ( a = x1 & x1 in A1 & not x1 in B1 ) ; hence a in A1 \ B1 by XBOOLE_0:def_5; ::_thesis: verum end; theorem Th31: :: DOMAIN_1:31 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } thus A1 \+\ B1 c= { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } :: according to XBOOLE_0:def_10 ::_thesis: { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } c= A1 \+\ B1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 \+\ B1 or a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } ) assume A1: a in A1 \+\ B1 ; ::_thesis: a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } then reconsider x = a as Element of X1 ; ( ( x in A1 & not x in B1 ) or ( not x in A1 & x in B1 ) ) by A1, XBOOLE_0:1; hence a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } or a in A1 \+\ B1 ) assume a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } ; ::_thesis: a in A1 \+\ B1 then ex x1 being Element of X1 st ( a = x1 & ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) ) ; hence a in A1 \+\ B1 by XBOOLE_0:1; ::_thesis: verum end; theorem Th32: :: DOMAIN_1:32 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } A1: for x1 being Element of X1 holds ( ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) iff ( not x1 in A1 iff x1 in B1 ) ) ; defpred S1[ set ] means ( not \$1 in A1 iff \$1 in B1 ); defpred S2[ set ] means ( ( \$1 in A1 & not \$1 in B1 ) or ( not \$1 in A1 & \$1 in B1 ) ); A2: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } by Th31; for X1 being non empty set st ( for x1 being Element of X1 holds ( S2[x1] iff S1[x1] ) ) holds { y1 where y1 is Element of X1 : S2[y1] } = { z1 where z1 is Element of X1 : S1[z1] } from DOMAIN_1:sch_6(); hence A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } by A1, A2; ::_thesis: verum end; theorem :: DOMAIN_1:33 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 ) } let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 ) } A1: for x1 being Element of X1 holds ( not ( ( not x1 in A1 implies x1 in B1 ) & ( x1 in B1 implies not x1 in A1 ) & not ( x1 in A1 iff not x1 in B1 ) ) & not ( ( x1 in A1 implies not x1 in B1 ) & ( not x1 in B1 implies x1 in A1 ) & not ( not x1 in A1 iff x1 in B1 ) ) ) ; defpred S1[ set ] means ( \$1 in A1 iff not \$1 in B1 ); defpred S2[ set ] means ( not \$1 in A1 iff \$1 in B1 ); A2: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } by Th32; for X1 being non empty set st ( for x1 being Element of X1 holds ( S2[x1] iff S1[x1] ) ) holds { y1 where y1 is Element of X1 : S2[y1] } = { z1 where z1 is Element of X1 : S1[z1] } from DOMAIN_1:sch_6(); hence A1 \+\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 ) } by A1, A2; ::_thesis: verum end; theorem :: DOMAIN_1:34 for X1 being non empty set for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) } proof let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) } let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) } A1: for x1 being Element of X1 holds ( ( not x1 in A1 iff x1 in B1 ) iff ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) ) ; defpred S1[ set ] means ( ( \$1 in A1 & not \$1 in B1 ) or ( \$1 in B1 & not \$1 in A1 ) ); defpred S2[ set ] means ( not \$1 in A1 iff \$1 in B1 ); A2: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } by Th32; for X1 being non empty set st ( for x1 being Element of X1 holds ( S2[x1] iff S1[x1] ) ) holds { y1 where y1 is Element of X1 : S2[y1] } = { z1 where z1 is Element of X1 : S1[z1] } from DOMAIN_1:sch_6(); hence A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) } by A1, A2; ::_thesis: verum end; definition let D be non empty set ; let x1 be Element of D; :: original: { redefine func{x1} -> Subset of D; coherence {x1} is Subset of D by SUBSET_1:33; let x2 be Element of D; :: original: { redefine func{x1,x2} -> Subset of D; coherence {x1,x2} is Subset of D by SUBSET_1:34; let x3 be Element of D; :: original: { redefine func{x1,x2,x3} -> Subset of D; coherence {x1,x2,x3} is Subset of D by SUBSET_1:35; let x4 be Element of D; :: original: { redefine func{x1,x2,x3,x4} -> Subset of D; coherence {x1,x2,x3,x4} is Subset of D by SUBSET_1:36; let x5 be Element of D; :: original: { redefine func{x1,x2,x3,x4,x5} -> Subset of D; coherence {x1,x2,x3,x4,x5} is Subset of D by SUBSET_1:37; let x6 be Element of D; :: original: { redefine func{x1,x2,x3,x4,x5,x6} -> Subset of D; coherence {x1,x2,x3,x4,x5,x6} is Subset of D by SUBSET_1:38; let x7 be Element of D; :: original: { redefine func{x1,x2,x3,x4,x5,x6,x7} -> Subset of D; coherence {x1,x2,x3,x4,x5,x6,x7} is Subset of D by SUBSET_1:39; let x8 be Element of D; :: original: { redefine func{x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of D; coherence {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of D by SUBSET_1:40; end; begin scheme :: DOMAIN_1:sch 8 SubsetFD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } : { F3(x) where x is Element of F1() : P1[x] } is Subset of F2() proof set X = { F3(x) where x is Element of F1() : P1[x] } ; { F3(x) where x is Element of F1() : P1[x] } c= F2() proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { F3(x) where x is Element of F1() : P1[x] } or y in F2() ) assume y in { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in F2() then ex z being Element of F1() st ( y = F3(z) & P1[z] ) ; hence y in F2() ; ::_thesis: verum end; hence { F3(x) where x is Element of F1() : P1[x] } is Subset of F2() ; ::_thesis: verum end; scheme :: DOMAIN_1:sch 9 SubsetFD2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F3(), P1[ set , set ] } : { F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } is Subset of F3() proof set X = { F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } ; { F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } c= F3() proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in { F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } or w in F3() ) assume w in { F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } ; ::_thesis: w in F3() then ex x being Element of F1() ex y being Element of F2() st ( w = F4(x,y) & P1[x,y] ) ; hence w in F3() ; ::_thesis: verum end; hence { F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } is Subset of F3() ; ::_thesis: verum end; definition let D1, D2, D3 be non empty set ; let x be Element of [:[:D1,D2:],D3:]; :: original: `11 redefine funcx `11 -> Element of D1; coherence x `11 is Element of D1 proof x `11 = (x `1) `1 by MCART_1:def_14; hence x `11 is Element of D1 ; ::_thesis: verum end; :: original: `12 redefine funcx `12 -> Element of D2; coherence x `12 is Element of D2 proof x `12 = (x `1) `2 by MCART_1:def_15; hence x `12 is Element of D2 ; ::_thesis: verum end; end; definition let D1, D2, D3 be non empty set ; let x be Element of [:D1,[:D2,D3:]:]; :: original: `21 redefine funcx `21 -> Element of D2; coherence x `21 is Element of D2 proof x `21 = (x `2) `1 by MCART_1:def_16; hence x `21 is Element of D2 ; ::_thesis: verum end; :: original: `22 redefine funcx `22 -> Element of D3; coherence x `22 is Element of D3 proof x `22 = (x `2) `2 by MCART_1:def_17; hence x `22 is Element of D3 ; ::_thesis: verum end; end; scheme :: DOMAIN_1:sch 10 AndScheme{ F1() -> non empty set , P1[ set ], P2[ set ] } : { a where a is Element of F1() : ( P1[a] & P2[a] ) } = { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } proof set A = { a where a is Element of F1() : ( P1[a] & P2[a] ) } ; set A1 = { a1 where a1 is Element of F1() : P1[a1] } ; set A2 = { a2 where a2 is Element of F1() : P2[a2] } ; thus { a where a is Element of F1() : ( P1[a] & P2[a] ) } c= { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } :: according to XBOOLE_0:def_10 ::_thesis: { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } c= { a where a is Element of F1() : ( P1[a] & P2[a] ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } or x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } ) assume x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } ; ::_thesis: x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } then consider a being Element of F1() such that A1: x = a and A2: ( P1[a] & P2[a] ) ; ( a in { a1 where a1 is Element of F1() : P1[a1] } & a in { a2 where a2 is Element of F1() : P2[a2] } ) by A2; hence x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } by A1, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } or x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } ) assume A3: x in { a1 where a1 is Element of F1() : P1[a1] } /\ { a2 where a2 is Element of F1() : P2[a2] } ; ::_thesis: x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } then x in { a2 where a2 is Element of F1() : P2[a2] } by XBOOLE_0:def_4; then A4: ex a being Element of F1() st ( x = a & P2[a] ) ; x in { a1 where a1 is Element of F1() : P1[a1] } by A3, XBOOLE_0:def_4; then ex a being Element of F1() st ( x = a & P1[a] ) ; hence x in { a where a is Element of F1() : ( P1[a] & P2[a] ) } by A4; ::_thesis: verum end; registration let A be non empty set ; cluster non empty c=-linear for Element of bool A; existence ex b1 being Subset of A st ( b1 is c=-linear & not b1 is empty ) proof set a = the Element of A; reconsider B = { the Element of A} as non empty Subset of A ; take B ; ::_thesis: ( B is c=-linear & not B is empty ) B is c=-linear proof let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not x in B or not y in B or x,y are_c=-comparable ) assume that A1: x in B and A2: y in B ; ::_thesis: x,y are_c=-comparable x = the Element of A by A1, TARSKI:def_1; hence x,y are_c=-comparable by A2, TARSKI:def_1; ::_thesis: verum end; hence ( B is c=-linear & not B is empty ) ; ::_thesis: verum end; end;