let X be set ; :: thesis: for A, B, C being Subset of X ex F being Function of NAT ,(bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
let A, B, C be Subset of X; :: thesis: ex F being Function of NAT ,(bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
defpred S1[ Element of NAT , set ] means ( ( $1 = 0 implies $2 = A ) & ( $1 = 1 implies $2 = B ) & ( 1 < $1 implies $2 = C ) );
defpred S2[ set ] means ex n being Element of NAT ex X being set st
( $1 = [n,X] & S1[n,X] );
ex GRAF being set st
for x being set holds
( x in GRAF iff ( x in [:NAT ,(bool X):] & S2[x] ) ) from XBOOLE_0:sch 1();
 then consider GRAF being set such that
A1: for x being set holds
( x in GRAF iff ( x in [:NAT ,(bool X):] & S2[x] ) ) ;
A2: for x being set holds
( x in GRAF iff ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) )
proof
let x be set ; :: thesis: ( x in GRAF iff ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) )
A3: ( not x in GRAF or x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) )
proof
assume x in GRAF ; :: thesis: ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) )
then consider n being Element of NAT such that
A4: ex X0 being set st
( x = [n,X0] & S1[n,X0] ) by A1;
thus ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) by A4, NAT_1:26; :: thesis: verum
end;
( ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) implies x in GRAF )
proof
assume A5: ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) ; :: thesis: x in GRAF
A6: ( x = [0 ,A] implies x in GRAF )
proof
assume x = [0 ,A] ; :: thesis: x in GRAF
then ( x in [:NAT ,(bool X):] & S2[x] ) by ZFMISC_1:106;
hence x in GRAF by A1; :: thesis: verum
end;
A7: ( x = [1,B] implies x in GRAF )
proof
assume x = [1,B] ; :: thesis: x in GRAF
then ( x in [:NAT ,(bool X):] & S2[x] ) by ZFMISC_1:106;
hence x in GRAF by A1; :: thesis: verum
end;
( ex n being Element of NAT st
( x = [n,C] & 1 < n ) implies x in GRAF )
proof
given n being Element of NAT such that A8: ( x = [n,C] & 1 < n ) ; :: thesis: x in GRAF
S1[n,C] by A8;
then ( x in [:NAT ,(bool X):] & S2[x] ) by A8, ZFMISC_1:106;
hence x in GRAF by A1; :: thesis: verum
end;
hence x in GRAF by A5, A6, A7; :: thesis: verum
end;
hence ( x in GRAF iff ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) ) by A3; :: thesis: verum
end;
A9: GRAF is Relation-like
proof
let p be set ; :: according to RELAT_1:def 1 :: thesis: ( not p in GRAF or ex b1, b2 being set st p = [b1,b2] )
assume p in GRAF ; :: thesis: ex b1, b2 being set st p = [b1,b2]
then ( p = [0 ,A] or p = [1,B] or ex n being Element of NAT st
( p = [n,C] & 1 < n ) ) by A2;
hence ex b1, b2 being set st p = [b1,b2] ; :: thesis: verum
end;
GRAF is Function-like
proof
let x, y1, y2 be set ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in GRAF or not [x,y2] in GRAF or y1 = y2 )
assume A10: ( [x,y1] in GRAF & [x,y2] in GRAF ) ; :: thesis: y1 = y2
then A11: ( [x,y1] in [:NAT ,(bool X):] & S2[[x,y1]] ) by A1;
A12: ( [x,y2] in [:NAT ,(bool X):] & S2[[x,y2]] ) by A1, A10;
then reconsider x = x as Element of NAT by ZFMISC_1:106;
per cases ( x = 0 or x = 1 or x > 1 ) by NAT_1:26;
end;
end;
then reconsider F = GRAF as Function by A9;
A16: dom F = NAT
proof
for x being set holds
( x in NAT iff ex y being set st [x,y] in F )
proof
let x be set ; :: thesis: ( x in NAT iff ex y being set st [x,y] in F )
thus ( x in NAT implies ex y being set st [x,y] in F ) :: thesis: ( ex y being set st [x,y] in F implies x in NAT )
proof
assume x in NAT ; :: thesis: ex y being set st [x,y] in F
then reconsider x = x as Element of NAT ;
A17: ( x = 0 implies ex y being set st [x,y] in F )
proof
assume A18: x = 0 ; :: thesis: ex y being set st [x,y] in F
take A ; :: thesis: [x,A] in F
thus [x,A] in F by A2, A18; :: thesis: verum
end;
A19: ( x = 1 implies ex y being set st [x,y] in F )
proof
assume A20: x = 1 ; :: thesis: ex y being set st [x,y] in F
take B ; :: thesis: [x,B] in F
thus [x,B] in F by A2, A20; :: thesis: verum
end;
( 1 < x implies ex y being set st [x,y] in F )
proof
assume A21: 1 < x ; :: thesis: ex y being set st [x,y] in F
take C ; :: thesis: [x,C] in F
thus [x,C] in F by A2, A21; :: thesis: verum
end;
hence ex y being set st [x,y] in F by A17, A19, NAT_1:26; :: thesis: verum
end;
given y being set such that A22: [x,y] in F ; :: thesis: x in NAT
[x,y] in [:NAT ,(bool X):] by A1, A22;
hence x in NAT by ZFMISC_1:106; :: thesis: verum
end;
hence dom F = NAT by RELAT_1:def 4; :: thesis: verum
end;
A23: rng F = {A,B,C}
proof
for y being set holds
( y in {A,B,C} iff ex x being set st
( x in dom F & y = F . x ) )
proof
let y be set ; :: thesis: ( y in {A,B,C} iff ex x being set st
( x in dom F & y = F . x ) )
thus ( y in {A,B,C} implies ex x being set st
( x in dom F & y = F . x ) ) :: thesis: ( ex x being set st
( x in dom F & y = F . x ) implies y in {A,B,C} )
proof
assume A24: y in {A,B,C} ; :: thesis: ex x being set st
( x in dom F & y = F . x )
per cases ( y = A or y = B or y = C ) by A24, ENUMSET1:def 1;
suppose y = A ; :: thesis: ex x being set st
( x in dom F & y = F . x )
then A25: [0 ,y] in F by A2;
take 0 ; :: thesis: ( 0 in dom F & y = F . 0 )
thus ( 0 in dom F & y = F . 0 ) by A25, FUNCT_1:8; :: thesis: verum
end;
suppose y = B ; :: thesis: ex x being set st
( x in dom F & y = F . x )
then A26: [1,y] in F by A2;
take 1 ; :: thesis: ( 1 in dom F & y = F . 1 )
thus ( 1 in dom F & y = F . 1 ) by A26, FUNCT_1:8; :: thesis: verum
end;
suppose y = C ; :: thesis: ex x being set st
( x in dom F & y = F . x )
then A27: [2,y] in F by A2;
take 2 ; :: thesis: ( 2 in dom F & y = F . 2 )
thus ( 2 in dom F & y = F . 2 ) by A27, FUNCT_1:8; :: thesis: verum
end;
end;
end;
given x being set such that A28: ( x in dom F & y = F . x ) ; :: thesis: y in {A,B,C}
reconsider x = x as Element of NAT by A16, A28;
per cases ( x = 0 or x = 1 or 1 < x ) by NAT_1:26;
suppose A30: x = 1 ; :: thesis: y in {A,B,C}
[1,B] in F by A2;
then B = F . x by A30, FUNCT_1:8;
hence y in {A,B,C} by A28, ENUMSET1:def 1; :: thesis: verum
end;
end;
end;
hence rng F = {A,B,C} by FUNCT_1:def 5; :: thesis: verum
end;
rng F c= bool X
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng F or a in bool X )
assume a in rng F ; :: thesis: a in bool X
then ( a = A or a = B or a = C ) by A23, ENUMSET1:def 1;
hence a in bool X ; :: thesis: verum
end;
then reconsider F = F as Function of NAT ,(bool X) by A16, FUNCT_2:4;
take F ; :: thesis: ( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
( F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
proof
A31: [0 ,A] in F by A2;
A32: [1,B] in F by A2;
for n being Element of NAT st 1 < n holds
F . n = C
proof
let n be Element of NAT ; :: thesis: ( 1 < n implies F . n = C )
assume 1 < n ; :: thesis: F . n = C
then [n,C] in F by A2;
hence F . n = C by FUNCT_1:8; :: thesis: verum
end;
hence ( F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) ) by A31, A32, FUNCT_1:8; :: thesis: verum
end;
hence ( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) ) by A23; :: thesis: verum