let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being natural number st 1 <= i & i <= len s holds
[((apply s,t) . (i + 1)),((apply s,t) . i)] in T @-->
let t be type of T; :: thesis: for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being natural number st 1 <= i & i <= len s holds
[((apply s,t) . (i + 1)),((apply s,t) . i)] in T @-->
let A be finite Subset of the adjectives of T; :: thesis: ( ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) implies for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being natural number st 1 <= i & i <= len s holds
[((apply s,t) . (i + 1)),((apply s,t) . i)] in T @--> )
assume A1:
for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A
; :: thesis: for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being natural number st 1 <= i & i <= len s holds
[((apply s,t) . (i + 1)),((apply s,t) . i)] in T @-->
let s be one-to-one FinSequence of the adjectives of T; :: thesis: ( rng s = A & s is_properly_applicable_to t implies for i being natural number st 1 <= i & i <= len s holds
[((apply s,t) . (i + 1)),((apply s,t) . i)] in T @--> )
assume A2:
( rng s = A & s is_properly_applicable_to t )
; :: thesis: for i being natural number st 1 <= i & i <= len s holds
[((apply s,t) . (i + 1)),((apply s,t) . i)] in T @-->
A3:
len (apply s,t) = (len s) + 1
by Def19;
let j be natural number ; :: thesis: ( 1 <= j & j <= len s implies [((apply s,t) . (j + 1)),((apply s,t) . j)] in T @--> )
assume A4:
( 1 <= j & j <= len s )
; :: thesis: [((apply s,t) . (j + 1)),((apply s,t) . j)] in T @-->
then
( j < (len s) + 1 & j is Element of NAT )
by NAT_1:13, ORDINAL1:def 13;
then A5:
( j in dom s & j in dom (apply s,t) )
by A3, A4, FINSEQ_3:27;
then
( s . j in rng s & rng s c= the adjectives of T )
by FUNCT_1:12;
then reconsider a = s . j as adjective of T ;
( (apply s,t) . j in rng (apply s,t) & rng (apply s,t) c= the carrier of T )
by A5, FUNCT_1:12;
then reconsider tt = (apply s,t) . j as type of T ;
A6:
( (apply s,t) . (j + 1) = a ast tt & a is_properly_applicable_to tt )
by A2, A5, Def19, Def28;
not a in adjs tt
proof
assume A7:
a in adjs tt
;
:: thesis: contradiction
consider i being
Nat such that A8:
j = 1
+ i
by A4, NAT_1:10;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
reconsider s1 =
s | (Seg i) as
FinSequence of the
adjectives of
T by FINSEQ_1:23;
s1 c= s
by TREES_1:def 1;
then consider s2 being
FinSequence such that A9:
s = s1 ^ s2
by TREES_1:8;
reconsider s2 =
s2 as
FinSequence of the
adjectives of
T by A9, FINSEQ_1:50;
reconsider s21 =
s2 | (Seg 1) as
FinSequence of the
adjectives of
T by FINSEQ_1:23;
i <= len s
by A4, A8, NAT_1:13;
then A10:
(
len s = (len s1) + (len s2) &
len s1 = i )
by A9, FINSEQ_1:21, FINSEQ_1:35;
then A11:
len s2 >= 1
by A4, A8, XREAL_1:8;
then A12:
len s21 = 1
by FINSEQ_1:21;
then A13:
s21 = <*(s21 . 1)*>
by FINSEQ_1:57;
then A14:
rng s21 = {(s21 . 1)}
by FINSEQ_1:56;
then reconsider b =
s21 . 1 as
adjective of
T by ZFMISC_1:37;
s21 c= s2
by TREES_1:def 1;
then consider s22 being
FinSequence such that A15:
s2 = s21 ^ s22
by TREES_1:8;
reconsider s22 =
s22 as
FinSequence of the
adjectives of
T by A15, FINSEQ_1:50;
A16:
1
in dom s2
by A11, FINSEQ_3:27;
A17:
b =
s2 . 1
by A13, A15, FINSEQ_1:58
.=
a
by A8, A9, A10, A16, FINSEQ_1:def 7
;
A18:
s1 is_properly_applicable_to t
by A2, A9, A10, Th61;
s1 ast t = tt
by A8, A9, A10, Th37;
then A19:
s1 ast t =
a ast (s1 ast t)
by A7, Th25
.=
s21 ast (s1 ast t)
by A13, A17, Th32
;
s2 is_properly_applicable_to s1 ast t
by A2, A9, Th61;
then
s22 is_properly_applicable_to s1 ast t
by A15, A19, Th61;
then A20:
s1 ^ s22 is_properly_applicable_to t
by A18, Th62;
reconsider B =
rng (s1 ^ s22) as
Subset of the
adjectives of
T ;
s ast t =
s2 ast (s1 ast t)
by A9, Th38
.=
s22 ast (s1 ast t)
by A15, A19, Th38
.=
(s1 ^ s22) ast t
by Th38
;
then A21:
A ast t =
(s1 ^ s22) ast t
by A2, Th57, Th58
.=
B ast t
by A20, Th57, Th58
;
A22:
B is_properly_applicable_to t
by A20, Def29;
A23:
(
B = (rng s1) \/ (rng s22) &
A = (rng s1) \/ (rng s2) &
rng s2 = (rng s21) \/ (rng s22) )
by A2, A9, A15, FINSEQ_1:44;
then
rng s22 c= rng s2
by XBOOLE_1:7;
then A24:
B = A
by A1, A21, A22, A23, XBOOLE_1:9;
a in rng s21
by A14, A17, TARSKI:def 1;
then
a in rng s2
by A23, XBOOLE_0:def 3;
then A25:
a in B
by A23, A24, XBOOLE_0:def 3;
per cases
( a in rng s1 or a in rng s22 )
by A23, A25, XBOOLE_0:def 3;
suppose
a in rng s22
;
:: thesis: contradictionthen consider x being
set such that A27:
(
x in dom s22 &
a = s22 . x )
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A27;
x >= 0 + 1
by A27, FINSEQ_3:27;
then A28:
(
(x + 1) + i = j + x &
j + x > j + 0 )
by A8, XREAL_1:8;
( 1
+ x in dom s2 &
s2 . (1 + x) = a )
by A12, A15, A27, FINSEQ_1:41, FINSEQ_1:def 7;
then
(
i + (1 + x) in dom s &
s . (i + (1 + x)) = a )
by A9, A10, FINSEQ_1:41, FINSEQ_1:def 7;
hence
contradiction
by A5, A28, FUNCT_1:def 8;
:: thesis: verum end;
end;
hence
[((apply s,t) . (j + 1)),((apply s,t) . j)] in T @-->
by A6, Def31; :: thesis: verum