let Al be QC-alphabet ; :: thesis: for PHI being finite Subset of (CQC-WFF Al) ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

let PHI be finite Subset of (CQC-WFF Al); :: thesis: ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

defpred S_{1}[ set ] means ( $1 is finite Subset of (CQC-WFF Al) implies ex Al1 being countable QC-alphabet st

( $1 is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) );

A1: PHI is finite ;

A2: S_{1}[ {} ]
_{1}[B] holds

S_{1}[B \/ {x}]
_{1}[PHI]
from FINSET_1:sch 2(A1, A2, A3);

hence ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) ; :: thesis: verum

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

let PHI be finite Subset of (CQC-WFF Al); :: thesis: ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

defpred S

( $1 is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) );

A1: PHI is finite ;

A2: S

proof

A3:
for x, B being set st x in PHI & B c= PHI & S
set Al1 = [:NAT,NAT:];

reconsider Al1 = [:NAT,NAT:] as countable QC-alphabet by QC_LANG1:def 1, CARD_4:7;

( Al = [:NAT,(QC-symbols Al):] & NAT c= QC-symbols Al ) by QC_LANG1:3, QC_LANG1:5;

then ( Al is Al1 -expanding & {} is finite Subset of (CQC-WFF Al1) ) by XBOOLE_1:2, ZFMISC_1:96;

hence S_{1}[ {} ]
; :: thesis: verum

end;reconsider Al1 = [:NAT,NAT:] as countable QC-alphabet by QC_LANG1:def 1, CARD_4:7;

( Al = [:NAT,(QC-symbols Al):] & NAT c= QC-symbols Al ) by QC_LANG1:3, QC_LANG1:5;

then ( Al is Al1 -expanding & {} is finite Subset of (CQC-WFF Al1) ) by XBOOLE_1:2, ZFMISC_1:96;

hence S

S

proof

S
let x, B be set ; :: thesis: ( x in PHI & B c= PHI & S_{1}[B] implies S_{1}[B \/ {x}] )

assume A4: ( x in PHI & B c= PHI & S_{1}[B] )
; :: thesis: S_{1}[B \/ {x}]

reconsider x = x as Element of CQC-WFF Al by A4;

reconsider B = B as finite Subset of (CQC-WFF Al) by A4, XBOOLE_1:1;

consider Al1 being countable QC-alphabet such that

A5: ( x is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by Th19;

consider Al2 being countable QC-alphabet such that

A6: ( B is finite Subset of (CQC-WFF Al2) & Al is Al2 -expanding ) by A4;

set Al3 = Al1 \/ Al2;

( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then A7: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;

NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by QC_LANG1:3, XBOOLE_1:10;

then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A7, QC_LANG1:def 1;

reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by Def1, CARD_2:85, XBOOLE_1:7;

consider x2 being Element of CQC-WFF Al1 such that

A8: x = x2 by A5;

for s being object st s in B holds

s in CQC-WFF Al3

then ( {x2} c= CQC-WFF Al3 & B c= CQC-WFF Al3 ) by ZFMISC_1:31;

then A11: B \/ {x} c= CQC-WFF Al3 by A8, XBOOLE_1:8;

( Al1 c= Al & Al2 c= Al ) by A5, A6;

then Al is Al3 -expanding QC-alphabet by Def1, XBOOLE_1:8;

hence S_{1}[B \/ {x}]
by A11; :: thesis: verum

end;assume A4: ( x in PHI & B c= PHI & S

reconsider x = x as Element of CQC-WFF Al by A4;

reconsider B = B as finite Subset of (CQC-WFF Al) by A4, XBOOLE_1:1;

consider Al1 being countable QC-alphabet such that

A5: ( x is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by Th19;

consider Al2 being countable QC-alphabet such that

A6: ( B is finite Subset of (CQC-WFF Al2) & Al is Al2 -expanding ) by A4;

set Al3 = Al1 \/ Al2;

( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then A7: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;

NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by QC_LANG1:3, XBOOLE_1:10;

then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A7, QC_LANG1:def 1;

reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by Def1, CARD_2:85, XBOOLE_1:7;

consider x2 being Element of CQC-WFF Al1 such that

A8: x = x2 by A5;

for s being object st s in B holds

s in CQC-WFF Al3

proof

then
( x2 is Element of CQC-WFF Al3 & B c= CQC-WFF Al3 )
by Th7;
let s be object ; :: thesis: ( s in B implies s in CQC-WFF Al3 )

assume A9: s in B ; :: thesis: s in CQC-WFF Al3

consider s2 being Element of CQC-WFF Al2 such that

A10: s = s2 by A6, A9;

s2 is Element of CQC-WFF Al3 by Th7;

hence s in CQC-WFF Al3 by A10; :: thesis: verum

end;assume A9: s in B ; :: thesis: s in CQC-WFF Al3

consider s2 being Element of CQC-WFF Al2 such that

A10: s = s2 by A6, A9;

s2 is Element of CQC-WFF Al3 by Th7;

hence s in CQC-WFF Al3 by A10; :: thesis: verum

then ( {x2} c= CQC-WFF Al3 & B c= CQC-WFF Al3 ) by ZFMISC_1:31;

then A11: B \/ {x} c= CQC-WFF Al3 by A8, XBOOLE_1:8;

( Al1 c= Al & Al2 c= Al ) by A5, A6;

then Al is Al3 -expanding QC-alphabet by Def1, XBOOLE_1:8;

hence S

hence ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) ; :: thesis: verum