now for x being object st x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} holds
x in Permutations 3let x be
object ;
( x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} implies x in Permutations 3 )A1:
idseq 3
in Permutations 3
by MATRIX_1:def 12;
A2:
<*3,1,2*> in Permutations 3
A3:
<*2,3,1*> in Permutations 3
A4:
<*1,3,2*> in Permutations 3
proof
reconsider h =
<*2,3*> as
FinSequence of
NAT ;
reconsider f =
<*1,2,3*> as
one-to-one FinSequence-like Function of
(Seg 3),
(Seg 3) by FINSEQ_2:53;
Rev h = <*3,2*>
by FINSEQ_5:61;
then
(
f = <*1*> ^ h &
<*1*> ^ (Rev h) = <*1,3,2*> )
by FINSEQ_1:43;
hence
<*1,3,2*> in Permutations 3
by A1, Th17, FINSEQ_2:53;
verum
end; A5:
<*2,1,3*> in Permutations 3
assume
x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
;
x in Permutations 3then
x in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
by ENUMSET1:12;
then
(
x in {<*1,2,3*>,<*3,2,1*>} or
x in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} )
by XBOOLE_0:def 3;
then
(
x in {<*1,2,3*>,<*3,2,1*>} or
x in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} )
by ENUMSET1:5;
then A6:
(
x in {<*1,2,3*>,<*3,2,1*>} or
x in {<*1,3,2*>,<*2,3,1*>} or
x in {<*2,1,3*>,<*3,1,2*>} )
by XBOOLE_0:def 3;
Rev (idseq 3) in Permutations 3
by Th4;
hence
x in Permutations 3
by A6, A1, A4, A3, A5, A2, Th15, FINSEQ_2:53, TARSKI:def 2;
verum end;
then A7:
{<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} c= Permutations 3
by TARSKI:def 3;
now for p being object st p in Permutations 3 holds
p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}let p be
object ;
( p in Permutations 3 implies p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} )assume
p in Permutations 3
;
p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}then reconsider q =
p as
Permutation of
(Seg 3) by MATRIX_1:def 12;
A8:
rng q = Seg 3
by FUNCT_2:def 3;
A9:
3
in Seg 3
;
then
q . 3
in Seg 3
by A8, FUNCT_2:4;
then A10:
(
q . 3
= 1 or
q . 3
= 2 or
q . 3
= 3 )
by ENUMSET1:def 1, FINSEQ_3:1;
A11:
2
in Seg 3
;
then
q . 2
in Seg 3
by A8, FUNCT_2:4;
then A12:
(
q . 2
= 1 or
q . 2
= 2 or
q . 2
= 3 )
by ENUMSET1:def 1, FINSEQ_3:1;
A13:
dom q = Seg 3
by FUNCT_2:52;
A14:
( ( not (
q . 1
= 1 &
q . 2
= 2 &
q . 3
= 3 ) & not (
q . 1
= 3 &
q . 2
= 2 &
q . 3
= 1 ) & not (
q . 1
= 1 &
q . 2
= 3 &
q . 3
= 2 ) & not (
q . 1
= 2 &
q . 2
= 3 &
q . 3
= 1 ) & not (
q . 1
= 2 &
q . 2
= 1 &
q . 3
= 3 ) & not (
q . 1
= 3 &
q . 2
= 1 &
q . 3
= 2 ) ) or
q = <*1,2,3*> or
q = <*3,2,1*> or
q = <*1,3,2*> or
q = <*2,3,1*> or
q = <*2,1,3*> or
q = <*3,1,2*> )
proof
reconsider q =
q as
FinSequence by A13, FINSEQ_1:def 2;
len q = 3
by A13, FINSEQ_1:def 3;
hence
( ( not (
q . 1
= 1 &
q . 2
= 2 &
q . 3
= 3 ) & not (
q . 1
= 3 &
q . 2
= 2 &
q . 3
= 1 ) & not (
q . 1
= 1 &
q . 2
= 3 &
q . 3
= 2 ) & not (
q . 1
= 2 &
q . 2
= 3 &
q . 3
= 1 ) & not (
q . 1
= 2 &
q . 2
= 1 &
q . 3
= 3 ) & not (
q . 1
= 3 &
q . 2
= 1 &
q . 3
= 2 ) ) or
q = <*1,2,3*> or
q = <*3,2,1*> or
q = <*1,3,2*> or
q = <*2,3,1*> or
q = <*2,1,3*> or
q = <*3,1,2*> )
by FINSEQ_1:45;
verum
end; A15:
1
in Seg 3
;
then
q . 1
in Seg 3
by A8, FUNCT_2:4;
then
(
q . 1
= 1 or
q . 1
= 2 or
q . 1
= 3 )
by ENUMSET1:def 1, FINSEQ_3:1;
then
(
p = <*1,2,3*> or
p = <*3,2,1*> or
q = <*1,3,2*> or
q = <*2,3,1*> or
q = <*2,1,3*> or
q = <*3,1,2*> )
by A13, A15, A11, A9, A12, A10, A14, FUNCT_1:def 4;
then
(
p in {<*1,2,3*>,<*3,2,1*>} or
q in {<*1,3,2*>,<*2,3,1*>} or
q in {<*2,1,3*>,<*3,1,2*>} )
by TARSKI:def 2;
then
(
p in {<*1,2,3*>,<*3,2,1*>} or
q in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} )
by XBOOLE_0:def 3;
then
(
p in {<*1,2,3*>,<*3,2,1*>} or
q in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} )
by ENUMSET1:5;
then
p in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
by XBOOLE_0:def 3;
hence
p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
by ENUMSET1:12;
verum end;
then
Permutations 3 c= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
by TARSKI:def 3;
hence
Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
by A7, XBOOLE_0:def 10; verum