let A be Universal_Algebra; for B being Subset of A
for n being Nat
for x being set holds
( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
let B be Subset of A; for n being Nat
for x being set holds
( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
defpred S1[ Nat] means for x being set holds
( not x in B |^ ($1 + 1) or x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ $1 ) );
A1:
B |^ 0 = B
by Th18;
then A2:
S1[ 0 ]
by Th20;
A3:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A4:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let x be
set ;
( not x in B |^ ((n + 1) + 1) or x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) ) )
assume
x in B |^ ((n + 1) + 1)
;
( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) ) )
then A5:
(
x in B |^ (n + 1) or ex
o being
Element of
dom the
charact of
A ex
p being
Element of the
carrier of
A * st
(
x = (Den (o,A)) . p &
p in dom (Den (o,A)) &
rng p c= B |^ (n + 1) ) )
by Th20;
now ( ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) implies ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) ) )given o being
Element of
dom the
charact of
A,
p being
Element of the
carrier of
A * such that A6:
x = (Den (o,A)) . p
and A7:
p in dom (Den (o,A))
and A8:
rng p c= B |^ n
;
ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) )take o =
o;
ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) )take p =
p;
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) )
n <= n + 1
by NAT_1:13;
then
B |^ n c= B |^ (n + 1)
by Th21;
hence
(
x = (Den (o,A)) . p &
p in dom (Den (o,A)) &
rng p c= B |^ (n + 1) )
by A6, A7, A8;
verum end;
hence
(
x in B or ex
o being
Element of
dom the
charact of
A ex
p being
Element of the
carrier of
A * st
(
x = (Den (o,A)) . p &
p in dom (Den (o,A)) &
rng p c= B |^ (n + 1) ) )
by A4, A5;
verum
end; end;
A9:
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
let n be Nat; for x being set holds
( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
let x be set ; ( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
B c= B |^ n
by A1, Th21;
hence
( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
by A9, Th20; verum