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 = SymGrp D
psgnval.t T = ran pmTrsp D
psgnval.n N = pmSgn D
Assertion psgnvali P dom N w Word T P = G w N P = 1 w

Proof

Step Hyp Ref Expression
1 psgnval.g G = SymGrp D
2 psgnval.t T = ran pmTrsp D
3 psgnval.n N = pmSgn D
4 1 2 3 psgnval P dom N N P = ι s | w Word T P = G w s = 1 w
5 1 2 3 psgneu P dom N ∃! s w Word T P = G w s = 1 w
6 iotacl ∃! s w Word T P = G w s = 1 w ι s | w Word T P = G w s = 1 w s | w Word T P = G w s = 1 w
7 5 6 syl P dom N ι s | w Word T P = G w s = 1 w s | w Word T P = G w s = 1 w
8 4 7 eqeltrd P dom N N P s | w Word T P = G w s = 1 w
9 fvex N P V
10 eqeq1 s = N P s = 1 w N P = 1 w
11 10 anbi2d s = N P P = G w s = 1 w P = G w N P = 1 w
12 11 rexbidv s = N P w Word T P = G w s = 1 w w Word T P = G w N P = 1 w
13 9 12 elab N P s | w Word T P = G w s = 1 w w Word T P = G w N P = 1 w
14 8 13 sylib P dom N w Word T P = G w N P = 1 w