Metamath Proof Explorer

Theorem subfacp1lem1

Description: Lemma for subfacp1 . The set K together with { 1 , M } partitions the set 1 ... ( N + 1 ) . (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Hypotheses derang.d 
|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
subfac.n 
|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
subfacp1lem.a 
|- A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
subfacp1lem1.n 
|- ( ph -> N e. NN )
subfacp1lem1.m 
|- ( ph -> M e. ( 2 ... ( N + 1 ) ) )
subfacp1lem1.x 
|- M e. _V
subfacp1lem1.k 
|- K = ( ( 2 ... ( N + 1 ) ) \ { M } )
Assertion subfacp1lem1 
|- ( ph -> ( ( K i^i { 1 , M } ) = (/) /\ ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) /\ ( # ` K ) = ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 derang.d 
 |-  D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2 subfac.n 
 |-  S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3 subfacp1lem.a 
 |-  A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
4 subfacp1lem1.n 
 |-  ( ph -> N e. NN )
5 subfacp1lem1.m 
 |-  ( ph -> M e. ( 2 ... ( N + 1 ) ) )
6 subfacp1lem1.x 
 |-  M e. _V
7 subfacp1lem1.k 
 |-  K = ( ( 2 ... ( N + 1 ) ) \ { M } )
8 disj 
 |-  ( ( K i^i { 1 , M } ) = (/) <-> A. x e. K -. x e. { 1 , M } )
9 eldifi 
 |-  ( x e. ( ( 2 ... ( N + 1 ) ) \ { M } ) -> x e. ( 2 ... ( N + 1 ) ) )
10 elfzle1 
 |-  ( x e. ( 2 ... ( N + 1 ) ) -> 2 <_ x )
11 1lt2 
 |-  1 < 2
12 1re 
 |-  1 e. RR
13 2re 
 |-  2 e. RR
14 12 13 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
15 11 14 mpbi 
 |-  -. 2 <_ 1
16 breq2 
 |-  ( x = 1 -> ( 2 <_ x <-> 2 <_ 1 ) )
17 15 16 mtbiri 
 |-  ( x = 1 -> -. 2 <_ x )
18 17 necon2ai 
 |-  ( 2 <_ x -> x =/= 1 )
19 9 10 18 3syl 
 |-  ( x e. ( ( 2 ... ( N + 1 ) ) \ { M } ) -> x =/= 1 )
20 eldifsni 
 |-  ( x e. ( ( 2 ... ( N + 1 ) ) \ { M } ) -> x =/= M )
21 19 20 jca 
 |-  ( x e. ( ( 2 ... ( N + 1 ) ) \ { M } ) -> ( x =/= 1 /\ x =/= M ) )
22 21 7 eleq2s 
 |-  ( x e. K -> ( x =/= 1 /\ x =/= M ) )
23 neanior 
 |-  ( ( x =/= 1 /\ x =/= M ) <-> -. ( x = 1 \/ x = M ) )
24 22 23 sylib 
 |-  ( x e. K -> -. ( x = 1 \/ x = M ) )
25 vex 
 |-  x e. _V
26 25 elpr 
 |-  ( x e. { 1 , M } <-> ( x = 1 \/ x = M ) )
27 24 26 sylnibr 
 |-  ( x e. K -> -. x e. { 1 , M } )
28 8 27 mprgbir 
 |-  ( K i^i { 1 , M } ) = (/)
29 28 a1i 
 |-  ( ph -> ( K i^i { 1 , M } ) = (/) )
30 uncom 
 |-  ( { 1 } u. ( K u. { M } ) ) = ( ( K u. { M } ) u. { 1 } )
31 1z 
 |-  1 e. ZZ
32 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
33 31 32 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
34 7 uneq1i 
 |-  ( K u. { M } ) = ( ( ( 2 ... ( N + 1 ) ) \ { M } ) u. { M } )
35 undif1 
 |-  ( ( ( 2 ... ( N + 1 ) ) \ { M } ) u. { M } ) = ( ( 2 ... ( N + 1 ) ) u. { M } )
36 34 35 eqtr2i 
 |-  ( ( 2 ... ( N + 1 ) ) u. { M } ) = ( K u. { M } )
37 33 36 uneq12i 
 |-  ( ( 1 ... 1 ) u. ( ( 2 ... ( N + 1 ) ) u. { M } ) ) = ( { 1 } u. ( K u. { M } ) )
38 df-pr 
 |-  { 1 , M } = ( { 1 } u. { M } )
39 38 equncomi 
 |-  { 1 , M } = ( { M } u. { 1 } )
40 39 uneq2i 
 |-  ( K u. { 1 , M } ) = ( K u. ( { M } u. { 1 } ) )
41 unass 
 |-  ( ( K u. { M } ) u. { 1 } ) = ( K u. ( { M } u. { 1 } ) )
42 40 41 eqtr4i 
 |-  ( K u. { 1 , M } ) = ( ( K u. { M } ) u. { 1 } )
43 30 37 42 3eqtr4i 
 |-  ( ( 1 ... 1 ) u. ( ( 2 ... ( N + 1 ) ) u. { M } ) ) = ( K u. { 1 , M } )
44 5 snssd 
 |-  ( ph -> { M } C_ ( 2 ... ( N + 1 ) ) )
45 ssequn2 
 |-  ( { M } C_ ( 2 ... ( N + 1 ) ) <-> ( ( 2 ... ( N + 1 ) ) u. { M } ) = ( 2 ... ( N + 1 ) ) )
46 44 45 sylib 
 |-  ( ph -> ( ( 2 ... ( N + 1 ) ) u. { M } ) = ( 2 ... ( N + 1 ) ) )
47 df-2 
 |-  2 = ( 1 + 1 )
48 47 oveq1i 
 |-  ( 2 ... ( N + 1 ) ) = ( ( 1 + 1 ) ... ( N + 1 ) )
49 46 48 eqtrdi 
 |-  ( ph -> ( ( 2 ... ( N + 1 ) ) u. { M } ) = ( ( 1 + 1 ) ... ( N + 1 ) ) )
50 49 uneq2d 
 |-  ( ph -> ( ( 1 ... 1 ) u. ( ( 2 ... ( N + 1 ) ) u. { M } ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
51 4 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
52 nnuz 
 |-  NN = ( ZZ>= ` 1 )
53 51 52 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
54 eluzfz1 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N + 1 ) ) )
55 fzsplit 
 |-  ( 1 e. ( 1 ... ( N + 1 ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
56 53 54 55 3syl 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
57 50 56 eqtr4d 
 |-  ( ph -> ( ( 1 ... 1 ) u. ( ( 2 ... ( N + 1 ) ) u. { M } ) ) = ( 1 ... ( N + 1 ) ) )
58 43 57 eqtr3id 
 |-  ( ph -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
59 47 oveq2i 
 |-  ( ( N + 1 ) - 2 ) = ( ( N + 1 ) - ( 1 + 1 ) )
60 fzfi 
 |-  ( 2 ... ( N + 1 ) ) e. Fin
61 diffi 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( ( 2 ... ( N + 1 ) ) \ { M } ) e. Fin )
62 60 61 ax-mp 
 |-  ( ( 2 ... ( N + 1 ) ) \ { M } ) e. Fin
63 7 62 eqeltri 
 |-  K e. Fin
64 prfi 
 |-  { 1 , M } e. Fin
65 hashun 
 |-  ( ( K e. Fin /\ { 1 , M } e. Fin /\ ( K i^i { 1 , M } ) = (/) ) -> ( # ` ( K u. { 1 , M } ) ) = ( ( # ` K ) + ( # ` { 1 , M } ) ) )
66 63 64 28 65 mp3an 
 |-  ( # ` ( K u. { 1 , M } ) ) = ( ( # ` K ) + ( # ` { 1 , M } ) )
67 58 fveq2d 
 |-  ( ph -> ( # ` ( K u. { 1 , M } ) ) = ( # ` ( 1 ... ( N + 1 ) ) ) )
68 neeq1 
 |-  ( x = M -> ( x =/= 1 <-> M =/= 1 ) )
69 10 18 syl 
 |-  ( x e. ( 2 ... ( N + 1 ) ) -> x =/= 1 )
70 68 69 vtoclga 
 |-  ( M e. ( 2 ... ( N + 1 ) ) -> M =/= 1 )
71 5 70 syl 
 |-  ( ph -> M =/= 1 )
72 71 necomd 
 |-  ( ph -> 1 =/= M )
73 1ex 
 |-  1 e. _V
74 hashprg 
 |-  ( ( 1 e. _V /\ M e. _V ) -> ( 1 =/= M <-> ( # ` { 1 , M } ) = 2 ) )
75 73 6 74 mp2an 
 |-  ( 1 =/= M <-> ( # ` { 1 , M } ) = 2 )
76 72 75 sylib 
 |-  ( ph -> ( # ` { 1 , M } ) = 2 )
77 76 oveq2d 
 |-  ( ph -> ( ( # ` K ) + ( # ` { 1 , M } ) ) = ( ( # ` K ) + 2 ) )
78 66 67 77 3eqtr3a 
 |-  ( ph -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( ( # ` K ) + 2 ) )
79 51 nnnn0d 
 |-  ( ph -> ( N + 1 ) e. NN0 )
80 hashfz1 
 |-  ( ( N + 1 ) e. NN0 -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
81 79 80 syl 
 |-  ( ph -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
82 78 81 eqtr3d 
 |-  ( ph -> ( ( # ` K ) + 2 ) = ( N + 1 ) )
83 51 nncnd 
 |-  ( ph -> ( N + 1 ) e. CC )
84 2cnd 
 |-  ( ph -> 2 e. CC )
85 hashcl 
 |-  ( K e. Fin -> ( # ` K ) e. NN0 )
86 63 85 ax-mp 
 |-  ( # ` K ) e. NN0
87 86 nn0cni 
 |-  ( # ` K ) e. CC
88 87 a1i 
 |-  ( ph -> ( # ` K ) e. CC )
89 83 84 88 subadd2d 
 |-  ( ph -> ( ( ( N + 1 ) - 2 ) = ( # ` K ) <-> ( ( # ` K ) + 2 ) = ( N + 1 ) ) )
90 82 89 mpbird 
 |-  ( ph -> ( ( N + 1 ) - 2 ) = ( # ` K ) )
91 4 nncnd 
 |-  ( ph -> N e. CC )
92 1cnd 
 |-  ( ph -> 1 e. CC )
93 91 92 92 pnpcan2d 
 |-  ( ph -> ( ( N + 1 ) - ( 1 + 1 ) ) = ( N - 1 ) )
94 59 90 93 3eqtr3a 
 |-  ( ph -> ( # ` K ) = ( N - 1 ) )
95 29 58 94 3jca 
 |-  ( ph -> ( ( K i^i { 1 , M } ) = (/) /\ ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) /\ ( # ` K ) = ( N - 1 ) ) )