set Y = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] } ;
set X = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ;
A2:
{ F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] } c= { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
proof
let x be
object ;
TARSKI:def 3 ( not x in { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] } or x in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } )
assume
x in { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
;
x in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
then consider u1 being
Element of
F1(),
v1 being
Element of
F2()
such that A3:
x = F4(
u1,
v1)
and A4:
P1[
u1,
v1]
;
x = F3(
u1,
v1)
by A1, A3;
hence
x in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
by A4;
verum
end;
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } c= { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
proof
let x be
object ;
TARSKI:def 3 ( not x in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } or x in { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] } )
assume
x in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
;
x in { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
then consider u1 being
Element of
F1(),
v1 being
Element of
F2()
such that A5:
x = F3(
u1,
v1)
and A6:
P1[
u1,
v1]
;
x = F4(
u1,
v1)
by A1, A5;
hence
x in { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
by A6;
verum
end;
hence
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
by A2; verum