Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem2b Structured version   Unicode version

Theorem subfacp1lem2b 24867
 Description: Lemma for subfacp1 24872. Properties of a bijection on augmented with the two-element flip to get a bijection on . (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
derang.d
subfac.n
subfacp1lem.a
subfacp1lem1.n
subfacp1lem1.m
subfacp1lem1.x
subfacp1lem1.k
subfacp1lem2.5
subfacp1lem2.6
Assertion
Ref Expression
subfacp1lem2b
Distinct variable groups:   ,,,,   ,,,   ,,,,   ,,   ,   ,,,,   ,,,   ,,,
Allowed substitution hints:   (,)   (,,)   ()   ()   (,,,)   ()   (,,,)

Proof of Theorem subfacp1lem2b
StepHypRef Expression
1 derang.d . . . . . 6
2 subfac.n . . . . . 6
3 subfacp1lem.a . . . . . 6
4 subfacp1lem1.n . . . . . 6
5 subfacp1lem1.m . . . . . 6
6 subfacp1lem1.x . . . . . 6
7 subfacp1lem1.k . . . . . 6
8 subfacp1lem2.5 . . . . . 6
9 subfacp1lem2.6 . . . . . 6
101, 2, 3, 4, 5, 6, 7, 8, 9subfacp1lem2a 24866 . . . . 5
1110simp1d 969 . . . 4
12 f1ofun 5676 . . . 4
1311, 12syl 16 . . 3