let V be Universe; for a being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
let a be Element of V; for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
let X be Subclass of V; for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
let fs be finite Subset of omega; ( X is closed_wrt_A1-A7 & a in X implies Funcs (fs,a) in X )
defpred S1[ set ] means Funcs ($1,a) in X;
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
a in X
; Funcs (fs,a) in X
A3:
X is closed_wrt_A4
by A1;
A4:
X is closed_wrt_A5
by A1;
A5:
for o, B being set st o in fs & B c= fs & S1[B] holds
S1[B \/ {o}]
proof
let o,
B be
set ;
( o in fs & B c= fs & S1[B] implies S1[B \/ {o}] )
assume that A6:
o in fs
and
B c= fs
and A7:
Funcs (
B,
a)
in X
;
S1[B \/ {o}]
per cases
( B meets {o} or B misses {o} )
;
suppose A8:
B misses {o}
;
S1[B \/ {o}]set r =
{o};
set A =
{ {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ;
A9:
(
omega c= X &
o in omega )
by A1, A6, Th7;
then
o in X
;
then reconsider p =
o as
Element of
V ;
A10:
Funcs (
{o},
a)
= { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
proof
thus
Funcs (
{o},
a)
c= { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
XBOOLE_0:def 10 { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } c= Funcs ({o},a)proof
let q be
object ;
TARSKI:def 3 ( not q in Funcs ({o},a) or q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } )
assume
q in Funcs (
{o},
a)
;
q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
then consider g being
Function such that A11:
q = g
and A12:
dom g = {o}
and A13:
rng g c= a
by FUNCT_2:def 2;
o in dom g
by A12, TARSKI:def 1;
then A14:
g . o in rng g
by FUNCT_1:def 3;
then reconsider s =
g . o as
Element of
V by A2, A13, Th1;
(
o in {o} &
g = {[p,s]} )
by A12, GRFUNC_1:7, TARSKI:def 1;
hence
q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
by A11, A13, A14;
verum
end;
let q be
object ;
TARSKI:def 3 ( not q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } or q in Funcs ({o},a) )
assume
q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
;
q in Funcs ({o},a)
then consider x,
y being
Element of
V such that A15:
q = {[x,y]}
and A16:
x in {o}
and A17:
y in a
;
reconsider g =
q as
Function by A15;
rng g = {y}
by A15, RELAT_1:9;
then A18:
rng g c= a
by A17, ZFMISC_1:31;
x = o
by A16, TARSKI:def 1;
then
dom g = {o}
by A15, RELAT_1:9;
hence
q in Funcs (
{o},
a)
by A18, FUNCT_2:def 2;
verum
end; reconsider x =
Funcs (
B,
a) as
Element of
V by A7;
{o} in X
by A1, A9, Th2;
then A19:
Funcs (
{o},
a)
in X
by A2, A3, A10;
then reconsider y =
Funcs (
{o},
a) as
Element of
V ;
set Z =
{ (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } ;
Funcs (
(B \/ {o}),
a)
= { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }
proof
thus
Funcs (
(B \/ {o}),
a)
c= { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }
XBOOLE_0:def 10 { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } c= Funcs ((B \/ {o}),a)proof
let q be
object ;
TARSKI:def 3 ( not q in Funcs ((B \/ {o}),a) or q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } )
assume
q in Funcs (
(B \/ {o}),
a)
;
q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }
then consider g being
Function such that A20:
q = g
and A21:
dom g = B \/ {o}
and A22:
rng g c= a
by FUNCT_2:def 2;
set A =
g | B;
rng (g | B) c= rng g
by RELAT_1:70;
then A23:
rng (g | B) c= a
by A22;
set C =
g | {o};
rng (g | {o}) c= rng g
by RELAT_1:70;
then A24:
rng (g | {o}) c= a
by A22;
dom (g | {o}) =
(B \/ {o}) /\ {o}
by A21, RELAT_1:61
.=
{o}
by XBOOLE_1:21
;
then A25:
g | {o} in y
by A24, FUNCT_2:def 2;
then reconsider y9 =
g | {o} as
Element of
V by A19, Th1;
dom (g | B) =
(B \/ {o}) /\ B
by A21, RELAT_1:61
.=
B
by XBOOLE_1:21
;
then A26:
g | B in x
by A23, FUNCT_2:def 2;
then reconsider x9 =
g | B as
Element of
V by A7, Th1;
g =
g | (B \/ {o})
by A21
.=
(g | B) \/ (g | {o})
by RELAT_1:78
;
then
q = x9 \/ y9
by A20;
hence
q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }
by A26, A25;
verum
end;
let q be
object ;
TARSKI:def 3 ( not q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } or q in Funcs ((B \/ {o}),a) )
assume
q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }
;
q in Funcs ((B \/ {o}),a)
then consider x9,
y9 being
Element of
V such that A27:
q = x9 \/ y9
and A28:
x9 in x
and A29:
y9 in y
;
consider e being
Function such that A30:
x9 = e
and A31:
dom e = B
and A32:
rng e c= a
by A28, FUNCT_2:def 2;
consider g being
Function such that A33:
y9 = g
and A34:
dom g = {o}
and A35:
rng g c= a
by A29, FUNCT_2:def 2;
reconsider h =
e \/ g as
Function by A8, A31, A34, GRFUNC_1:13;
rng h = (rng e) \/ (rng g)
by RELAT_1:12;
then A36:
rng h c= a \/ a
by A32, A35, XBOOLE_1:13;
dom h = B \/ {o}
by A31, A34, XTUPLE_0:23;
hence
q in Funcs (
(B \/ {o}),
a)
by A27, A30, A33, A36, FUNCT_2:def 2;
verum
end; hence
S1[
B \/ {o}]
by A4, A7, A19;
verum end;
end;
( Funcs ({},a) = {{}} & {} in X )
by A1, Th3, FUNCT_5:57;
then A37:
S1[ {} ]
by A1, Th2;
A38:
fs is finite
;
thus
S1[fs]
from FINSET_1:sch 2(A38, A37, A5); verum