set M = { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } ;
deffunc H1( set ) -> set = F5(($1 `1 ),($1 `2 ));
consider f being Function such that
A4:
dom f = [:(F3() /\ F1()),(F4() /\ F2()):]
and
A5:
for y being set st y in [:(F3() /\ F1()),(F4() /\ F2()):] holds
f . y = H1(y)
from FUNCT_1:sch 3();
A6:
dom f = [:F3(),F4():] /\ [:F1(),F2():]
by A4, ZFMISC_1:123;
{ F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } = f .: [:F3(),F4():]
proof
thus
{ F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } c= f .: [:F3(),F4():]
:: according to XBOOLE_0:def 10 :: thesis: f .: [:F3(),F4():] c= { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } or x in f .: [:F3(),F4():] )
assume
x in { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) }
;
:: thesis: x in f .: [:F3(),F4():]
then consider u being
Element of
F1(),
v being
Element of
F2()
such that A7:
x = F5(
u,
v)
and A8:
(
u in F3() &
v in F4() )
;
A9:
[u,v] in [:F3(),F4():]
by A8, ZFMISC_1:106;
then A10:
[u,v] in dom f
by A6, XBOOLE_0:def 4;
(
[u,v] `1 = u &
[u,v] `2 = v )
by MCART_1:7;
then
f . u,
v = F5(
u,
v)
by A4, A5, A10;
hence
x in f .: [:F3(),F4():]
by A7, A9, A10, FUNCT_1:def 12;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in f .: [:F3(),F4():] or x in { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } )
assume
x in f .: [:F3(),F4():]
;
:: thesis: x in { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) }
then consider y being
set such that A11:
y in dom f
and A12:
y in [:F3(),F4():]
and A13:
x = f . y
by FUNCT_1:def 12;
reconsider y =
y as
Element of
[:F1(),F2():] by A6, A11, XBOOLE_0:def 4;
y = [(y `1 ),(y `2 )]
by MCART_1:23;
then A14:
(
y `1 in F3() &
y `2 in F4() )
by A12, ZFMISC_1:106;
x = F5(
(y `1 ),
(y `2 ))
by A4, A5, A11, A13;
hence
x in { F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) }
by A14;
:: thesis: verum
end;
hence
{ F5(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' in F4() ) } is finite
by A1, A2; :: thesis: verum