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 S₁[ Element of NAT , set ] means ( ( $1 = 0 implies $2 = A ) & ( $1 = 1 implies $2 = B ) & ( 1 < $1 implies $2 = C ) );
defpred S₂[ set ] means ex n being Element of NAT ex X being set st
( $1 = [n,X] & S₁[n,X] );
ex GRAF being set st
for x being set holds
( x in GRAF iff ( x in [:NAT ,(bool X):] & S₂[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):] & S₂[x] ) ) ;
A2: 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 that
A3: [x,y1] in GRAF and
A4: [x,y2] in GRAF ; :: thesis: y1 = y2
A5: S₂[[x,y1]] by A1, A3;
A6: [x,y2] in [:NAT ,(bool X):] by A1, A4;
A7: S₂[[x,y2]] by A1, A4;
reconsider x = x as Element of NAT by A6, ZFMISC_1:106;

per cases ( x = 0 or x = 1 or x > 1 ) by NAT_1:26;

suppose A8: x = 0 ; :: thesis: y1 = y2

then y1 = A by A5, ZFMISC_1:33;
hence y1 = y2 by A7, A8, ZFMISC_1:33; :: thesis: verum

end;

suppose A9: x = 1 ; :: thesis: y1 = y2

then y1 = B by A5, ZFMISC_1:33;
hence y1 = y2 by A7, A9, ZFMISC_1:33; :: thesis: verum

end;

suppose A10: x > 1 ; :: thesis: y1 = y2

then y1 = C by A5, ZFMISC_1:33;
hence y1 = y2 by A7, A10, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

A11: 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 ) ) )
A12: ( ( 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

A13: ( 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 A14: x = [n,C] and
A15: 1 < n ; :: thesis: x in GRAF
( S₁[n,C] & x in [:NAT ,(bool X):] ) by A14, A15, ZFMISC_1:106;
hence x in GRAF by A1, A14; :: thesis: verum

end;

A16: ( x = [1,B] implies x in GRAF )

proof

assume A17: x = [1,B] ; :: thesis: x in GRAF
then x in [:NAT ,(bool X):] by ZFMISC_1:106;
hence x in GRAF by A1, A17; :: thesis: verum

end;

A18: ( x = [0 ,A] implies x in GRAF )

proof

assume A19: x = [0 ,A] ; :: thesis: x in GRAF
then x in [:NAT ,(bool X):] by ZFMISC_1:106;
hence x in GRAF by A1, A19; :: thesis: verum

end;

assume ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) ; :: thesis: x in GRAF
hence x in GRAF by A18, A16, A13; :: thesis: verum

end;

( 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 ex n being Element of NAT ex X0 being set st
( x = [n,X0] & S₁[n,X0] ) by A1;
hence ( x = [0 ,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) by NAT_1:26; :: 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 A12; :: thesis: verum

end;

GRAF is Relation-like

proof

let p be set ; :: according to RELAT_1:def 1 :: thesis: ( not p in GRAF or ex b₁, b₂ being set st p = [b₁,b₂] )
assume p in GRAF ; :: thesis: ex b₁, b₂ being set st p = [b₁,b₂]
then ( p = [0 ,A] or p = [1,B] or ex n being Element of NAT st
( p = [n,C] & 1 < n ) ) by A11;
hence ex b₁, b₂ being set st p = [b₁,b₂] ; :: thesis: verum

end;

then reconsider F = GRAF as Function by A2;
A20: 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 ;
A21: ( x = 1 implies ex y being set st [x,y] in F )

proof

assume A22: 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 A11, A22; :: thesis: verum

end;

A23: ( 1 < x implies ex y being set st [x,y] in F )

proof

assume A24: 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 A11, A24; :: thesis: verum

end;

( x = 0 implies ex y being set st [x,y] in F )

proof

assume A25: 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 A11, A25; :: thesis: verum

end;

hence ex y being set st [x,y] in F by A21, A23, NAT_1:26; :: thesis: verum

end;

given y being set such that A26: [x,y] in F ; :: thesis: x in NAT
[x,y] in [:NAT ,(bool X):] by A1, A26;
hence x in NAT by ZFMISC_1:106; :: thesis: verum

end;

then A27: dom F = NAT by RELAT_1:def 4;
A28: 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 A29: 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 A29, ENUMSET1:def 1;

suppose A30: y = A ; :: thesis: ex x being set st
( x in dom F & y = F . x )

take 0 ; :: thesis: ( 0 in dom F & y = F . 0 )
[0 ,y] in F by A11, A30;
hence ( 0 in dom F & y = F . 0 ) by FUNCT_1:8; :: thesis: verum

end;

suppose A31: y = B ; :: thesis: ex x being set st
( x in dom F & y = F . x )

take 1 ; :: thesis: ( 1 in dom F & y = F . 1 )
[1,y] in F by A11, A31;
hence ( 1 in dom F & y = F . 1 ) by FUNCT_1:8; :: thesis: verum

end;

suppose A32: y = C ; :: thesis: ex x being set st
( x in dom F & y = F . x )

take 2 ; :: thesis: ( 2 in dom F & y = F . 2 )
[2,y] in F by A11, A32;
hence ( 2 in dom F & y = F . 2 ) by FUNCT_1:8; :: thesis: verum

end;

end;

end;

given x being set such that A33: x in dom F and
A34: y = F . x ; :: thesis: y in {A,B,C}
reconsider x = x as Element of NAT by A20, A33, RELAT_1:def 4;

per cases ( x = 0 or x = 1 or 1 < x ) by NAT_1:26;

suppose A35: x = 0 ; :: thesis: y in {A,B,C}

[0 ,A] in F by A11;
then A = F . x by A35, FUNCT_1:8;
hence y in {A,B,C} by A34, ENUMSET1:def 1; :: thesis: verum

end;

suppose A36: x = 1 ; :: thesis: y in {A,B,C}

[1,B] in F by A11;
then B = F . x by A36, FUNCT_1:8;
hence y in {A,B,C} by A34, ENUMSET1:def 1; :: thesis: verum

end;

suppose 1 < x ; :: thesis: y in {A,B,C}

then [x,C] in F by A11;
then y = C by A34, FUNCT_1:8;
hence y in {A,B,C} by ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

then A37: rng F = {A,B,C} by FUNCT_1:def 5;
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 A37, ENUMSET1:def 1;
hence a in bool X ; :: thesis: verum

end;

then reconsider F = F as Function of NAT ,(bool X) by A27, FUNCT_2:4;
A38: 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 A11;
hence F . n = C by FUNCT_1:8; :: thesis: verum

end;

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 ) )
( [0 ,A] in F & [1,B] in F ) by A11;
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 A28, A38, FUNCT_1:8, FUNCT_1:def 5; :: thesis: verum