consider N being Function such that
N is one-to-one
and
A1:
dom N = NAT
and
A2:
rng N = [:NAT,NAT:]
by Th5, WELLORD2:def 4;
deffunc H1( object ) -> set = F1(((N . $1) `1),((N . $1) `2));
consider f being Function such that
A3:
( dom f = NAT & ( for x being object st x in NAT holds
f . x = H1(x) ) )
from FUNCT_1:sch 3();
{ F1(n1,n2) where n1, n2 is Nat : P1[n1,n2] } c= rng f
proof
let x be
object ;
TARSKI:def 3 ( not x in { F1(n1,n2) where n1, n2 is Nat : P1[n1,n2] } or x in rng f )
assume
x in { F1(n1,n2) where n1, n2 is Nat : P1[n1,n2] }
;
x in rng f
then consider n1,
n2 being
Nat such that A4:
x = F1(
n1,
n2)
and
P1[
n1,
n2]
;
(
n1 in NAT &
n2 in NAT )
by ORDINAL1:def 12;
then
[n1,n2] in [:NAT,NAT:]
by ZFMISC_1:87;
then consider y being
object such that A5:
y in dom N
and A6:
[n1,n2] = N . y
by A2, FUNCT_1:def 3;
(
[n1,n2] `1 = n1 &
[n1,n2] `2 = n2 )
;
then
x = f . y
by A1, A3, A4, A5, A6;
hence
x in rng f
by A1, A3, A5, FUNCT_1:def 3;
verum
end;
hence
{ F1(n1,n2) where n1, n2 is Nat : P1[n1,n2] } is countable
by A3, CARD_3:93; verum