Metamath Proof Explorer


Theorem psgnvali

Description: A finitary permutation has at least one representation for its parity. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g G=SymGrpD
psgnval.t T=ranpmTrspD
psgnval.n N=pmSgnD
Assertion psgnvali PdomNwWordTP=GwNP=1w

Proof

Step Hyp Ref Expression
1 psgnval.g G=SymGrpD
2 psgnval.t T=ranpmTrspD
3 psgnval.n N=pmSgnD
4 1 2 3 psgnval PdomNNP=ιs|wWordTP=Gws=1w
5 1 2 3 psgneu PdomN∃!swWordTP=Gws=1w
6 iotacl ∃!swWordTP=Gws=1wιs|wWordTP=Gws=1ws|wWordTP=Gws=1w
7 5 6 syl PdomNιs|wWordTP=Gws=1ws|wWordTP=Gws=1w
8 4 7 eqeltrd PdomNNPs|wWordTP=Gws=1w
9 fvex NPV
10 eqeq1 s=NPs=1wNP=1w
11 10 anbi2d s=NPP=Gws=1wP=GwNP=1w
12 11 rexbidv s=NPwWordTP=Gws=1wwWordTP=GwNP=1w
13 9 12 elab NPs|wWordTP=Gws=1wwWordTP=GwNP=1w
14 8 13 sylib PdomNwWordTP=GwNP=1w