Metamath Proof Explorer

Theorem coe1mul2lem2

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypothesis coe1mul2lem2.h 
|- H = { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) }
Assertion coe1mul2lem2 
|- ( k e. NN0 -> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) )

Proof

Step Hyp Ref Expression
1 coe1mul2lem2.h 
 |-  H = { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) }
2 df1o2 
 |-  1o = { (/) }
3 nn0ex 
 |-  NN0 e. _V
4 0ex 
 |-  (/) e. _V
5 eqid 
 |-  ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) = ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) )
6 2 3 4 5 mapsnf1o2 
 |-  ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
7 f1of1 
 |-  ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 -> ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -1-1-> NN0 )
8 6 7 ax-mp 
 |-  ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -1-1-> NN0
9 1 ssrab3 
 |-  H C_ ( NN0 ^m 1o )
10 9 a1i 
 |-  ( k e. NN0 -> H C_ ( NN0 ^m 1o ) )
11 f1ores 
 |-  ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -1-1-> NN0 /\ H C_ ( NN0 ^m 1o ) ) -> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " H ) )
12 8 10 11 sylancr 
 |-  ( k e. NN0 -> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " H ) )
13 coe1mul2lem1 
 |-  ( ( k e. NN0 /\ d e. ( NN0 ^m 1o ) ) -> ( d oR <_ ( 1o X. { k } ) <-> ( d ` (/) ) e. ( 0 ... k ) ) )
14 13 rabbidva 
 |-  ( k e. NN0 -> { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } = { d e. ( NN0 ^m 1o ) | ( d ` (/) ) e. ( 0 ... k ) } )
15 fveq1 
 |-  ( c = d -> ( c ` (/) ) = ( d ` (/) ) )
16 15 eleq1d 
 |-  ( c = d -> ( ( c ` (/) ) e. ( 0 ... k ) <-> ( d ` (/) ) e. ( 0 ... k ) ) )
17 16 cbvrabv 
 |-  { c e. ( NN0 ^m 1o ) | ( c ` (/) ) e. ( 0 ... k ) } = { d e. ( NN0 ^m 1o ) | ( d ` (/) ) e. ( 0 ... k ) }
18 14 17 eqtr4di 
 |-  ( k e. NN0 -> { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } = { c e. ( NN0 ^m 1o ) | ( c ` (/) ) e. ( 0 ... k ) } )
19 5 mptpreima 
 |-  ( `' ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( 0 ... k ) ) = { c e. ( NN0 ^m 1o ) | ( c ` (/) ) e. ( 0 ... k ) }
20 18 1 19 3eqtr4g 
 |-  ( k e. NN0 -> H = ( `' ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( 0 ... k ) ) )
21 20 imaeq2d 
 |-  ( k e. NN0 -> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " H ) = ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( `' ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( 0 ... k ) ) ) )
22 f1ofo 
 |-  ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 -> ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 )
23 6 22 ax-mp 
 |-  ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0
24 fz0ssnn0 
 |-  ( 0 ... k ) C_ NN0
25 foimacnv 
 |-  ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 /\ ( 0 ... k ) C_ NN0 ) -> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( `' ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( 0 ... k ) ) ) = ( 0 ... k ) )
26 23 24 25 mp2an 
 |-  ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( `' ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " ( 0 ... k ) ) ) = ( 0 ... k )
27 21 26 eqtrdi 
 |-  ( k e. NN0 -> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " H ) = ( 0 ... k ) )
28 27 f1oeq3d 
 |-  ( k e. NN0 -> ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " H ) <-> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( 0 ... k ) ) )
29 resmpt 
 |-  ( H C_ ( NN0 ^m 1o ) -> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) = ( c e. H |-> ( c ` (/) ) ) )
30 f1oeq1 
 |-  ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) = ( c e. H |-> ( c ` (/) ) ) -> ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( 0 ... k ) <-> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) ) )
31 10 29 30 3syl 
 |-  ( k e. NN0 -> ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( 0 ... k ) <-> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) ) )
32 28 31 bitrd 
 |-  ( k e. NN0 -> ( ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) |` H ) : H -1-1-onto-> ( ( c e. ( NN0 ^m 1o ) |-> ( c ` (/) ) ) " H ) <-> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) ) )
33 12 32 mpbid 
 |-  ( k e. NN0 -> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) )