set f = (ArProg (199,210)) | 10;
set g = ArProg (199,210);
10 c= NAT
;
then B4:
10 c= dom (ArProg (199,210))
by FUNCT_2:def 1;
B0: dom ((ArProg (199,210)) | 10) =
(dom (ArProg (199,210))) /\ 10
by RELAT_1:61
.=
10
by B4, XBOOLE_1:28
;
WW:
{199,409,619,829,1039,1249,1459,1669,1879,2089} c= (rng ((ArProg (199,210)) | 10)) /\ SetPrimes
proof
let x be
object ;
TARSKI:def 3 ( not x in {199,409,619,829,1039,1249,1459,1669,1879,2089} or x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes )
assume HH:
x in {199,409,619,829,1039,1249,1459,1669,1879,2089}
;
x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes
then
x is
Prime
by XPRIMES1:199, XPRIMES1:409, XPRIMES1:619, XPRIMES1:829, XPRIMES1:1039, XPRIMES1:1249, XPRIMES1:1459, XPRIMES1:1669, XPRIMES1:1879, XPRIMES1:2089, ENUMSET1:def 8;
then
x in SetPrimes
by NEWTON:def 6;
hence
x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes
by XBOOLE_0:def 4, HH, RngForArProg;
verum
end;
WV:
{199,409,619,829,1039} misses {1249,1459,1669,1879,2089}
proof
assume
{199,409,619,829,1039} meets {1249,1459,1669,1879,2089}
;
contradiction
then consider x being
object such that F1:
(
x in {199,409,619,829,1039} &
x in {1249,1459,1669,1879,2089} )
by XBOOLE_0:3;
(
x = 199 or
x = 409 or
x = 619 or
x = 829 or
x = 1039 )
by F1, ENUMSET1:def 3;
hence
contradiction
by F1, ENUMSET1:def 3;
verum
end;
WZ:
199,409,619,829,1039 are_mutually_distinct
;
WA:
card {199,409,619,829,1039} = 5
by WZ, CARD_2:63;
1249,1459,1669,1879,2089 are_mutually_distinct
;
then WB:
card {1249,1459,1669,1879,2089} = 5
by CARD_2:63;
(rng ((ArProg (199,210)) | 10)) /\ SetPrimes c= {199,409,619,829,1039,1249,1459,1669,1879,2089}
proof
let x be
object ;
TARSKI:def 3 ( not x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes or x in {199,409,619,829,1039,1249,1459,1669,1879,2089} )
assume
x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes
;
x in {199,409,619,829,1039,1249,1459,1669,1879,2089}
then
(
x in rng ((ArProg (199,210)) | 10) &
x in SetPrimes )
by XBOOLE_0:def 4;
then consider y being
object such that B1:
(
y in dom ((ArProg (199,210)) | 10) &
x = ((ArProg (199,210)) | 10) . y )
by FUNCT_1:def 3;
B3:
x = (ArProg (199,210)) . y
by B0, B1, FUNCT_1:49;
(
y = 0 or
y = 1 or
y = 2 or
y = 3 or
y = 4 or
y = 5 or
y = 6 or
y = 7 or
y = 8 or
y = 9 )
by CARD_1:58, B0, B1, ENUMSET1:def 8;
hence
x in {199,409,619,829,1039,1249,1459,1669,1879,2089}
by ENUMSET1:def 8, B3, Th1990, Th1991, Th1992, Th1993, Th1994, Th1995, Th1996, Th1997, Th1998, Th1999;
verum
end;
then (rng ((ArProg (199,210)) | 10)) /\ SetPrimes =
{199,409,619,829,1039,1249,1459,1669,1879,2089}
by WW, XBOOLE_0:def 10
.=
{199,409,619,829,1039} \/ {1249,1459,1669,1879,2089}
by SetFor10
;
then card ((rng ((ArProg (199,210)) | 10)) /\ SetPrimes) =
(card {199,409,619,829,1039}) + (card {1249,1459,1669,1879,2089})
by CARD_2:40, WV
.=
10
by WA, WB
;
hence
card ((rng ((ArProg (199,210)) | 10)) /\ SetPrimes) = 10
; verum