Metamath Proof Explorer

Theorem fz1isolem

Description: Lemma for fz1iso . (Contributed by Mario Carneiro, 2-Apr-2014)

Ref Expression
Hypotheses fz1iso.1 
|- G = ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om )
fz1iso.2 
|- B = ( NN i^i ( `' < " { ( ( # ` A ) + 1 ) } ) )
fz1iso.3 
|- C = ( _om i^i ( `' G ` ( ( # ` A ) + 1 ) ) )
fz1iso.4 
|- O = OrdIso ( R , A )
Assertion fz1isolem 
|- ( ( R Or A /\ A e. Fin ) -> E. f f Isom < , R ( ( 1 ... ( # ` A ) ) , A ) )

Proof

Step Hyp Ref Expression
1 fz1iso.1 
 |-  G = ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om )
2 fz1iso.2 
 |-  B = ( NN i^i ( `' < " { ( ( # ` A ) + 1 ) } ) )
3 fz1iso.3 
 |-  C = ( _om i^i ( `' G ` ( ( # ` A ) + 1 ) ) )
4 fz1iso.4 
 |-  O = OrdIso ( R , A )
5 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
6 5 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( # ` A ) e. NN0 )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1z 
 |-  1 e. ZZ
9 8 1 om2uzisoi 
 |-  G Isom _E , < ( _om , ( ZZ>= ` 1 ) )
10 isoeq5 
 |-  ( NN = ( ZZ>= ` 1 ) -> ( G Isom _E , < ( _om , NN ) <-> G Isom _E , < ( _om , ( ZZ>= ` 1 ) ) ) )
11 9 10 mpbiri 
 |-  ( NN = ( ZZ>= ` 1 ) -> G Isom _E , < ( _om , NN ) )
12 7 11 ax-mp 
 |-  G Isom _E , < ( _om , NN )
13 isocnv 
 |-  ( G Isom _E , < ( _om , NN ) -> `' G Isom < , _E ( NN , _om ) )
14 12 13 ax-mp 
 |-  `' G Isom < , _E ( NN , _om )
15 nn0p1nn 
 |-  ( ( # ` A ) e. NN0 -> ( ( # ` A ) + 1 ) e. NN )
16 fvex 
 |-  ( `' G ` ( ( # ` A ) + 1 ) ) e. _V
17 16 epini 
 |-  ( `' _E " { ( `' G ` ( ( # ` A ) + 1 ) ) } ) = ( `' G ` ( ( # ` A ) + 1 ) )
18 17 ineq2i 
 |-  ( _om i^i ( `' _E " { ( `' G ` ( ( # ` A ) + 1 ) ) } ) ) = ( _om i^i ( `' G ` ( ( # ` A ) + 1 ) ) )
19 3 18 eqtr4i 
 |-  C = ( _om i^i ( `' _E " { ( `' G ` ( ( # ` A ) + 1 ) ) } ) )
20 2 19 isoini2 
 |-  ( ( `' G Isom < , _E ( NN , _om ) /\ ( ( # ` A ) + 1 ) e. NN ) -> ( `' G |` B ) Isom < , _E ( B , C ) )
21 14 15 20 sylancr 
 |-  ( ( # ` A ) e. NN0 -> ( `' G |` B ) Isom < , _E ( B , C ) )
22 6 21 syl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( `' G |` B ) Isom < , _E ( B , C ) )
23 nnz 
 |-  ( f e. NN -> f e. ZZ )
24 6 nn0zd 
 |-  ( ( R Or A /\ A e. Fin ) -> ( # ` A ) e. ZZ )
25 eluz 
 |-  ( ( f e. ZZ /\ ( # ` A ) e. ZZ ) -> ( ( # ` A ) e. ( ZZ>= ` f ) <-> f <_ ( # ` A ) ) )
26 23 24 25 syl2anr 
 |-  ( ( ( R Or A /\ A e. Fin ) /\ f e. NN ) -> ( ( # ` A ) e. ( ZZ>= ` f ) <-> f <_ ( # ` A ) ) )
27 zleltp1 
 |-  ( ( f e. ZZ /\ ( # ` A ) e. ZZ ) -> ( f <_ ( # ` A ) <-> f < ( ( # ` A ) + 1 ) ) )
28 23 24 27 syl2anr 
 |-  ( ( ( R Or A /\ A e. Fin ) /\ f e. NN ) -> ( f <_ ( # ` A ) <-> f < ( ( # ` A ) + 1 ) ) )
29 ovex 
 |-  ( ( # ` A ) + 1 ) e. _V
30 vex 
 |-  f e. _V
31 30 eliniseg 
 |-  ( ( ( # ` A ) + 1 ) e. _V -> ( f e. ( `' < " { ( ( # ` A ) + 1 ) } ) <-> f < ( ( # ` A ) + 1 ) ) )
32 29 31 ax-mp 
 |-  ( f e. ( `' < " { ( ( # ` A ) + 1 ) } ) <-> f < ( ( # ` A ) + 1 ) )
33 28 32 bitr4di 
 |-  ( ( ( R Or A /\ A e. Fin ) /\ f e. NN ) -> ( f <_ ( # ` A ) <-> f e. ( `' < " { ( ( # ` A ) + 1 ) } ) ) )
34 26 33 bitr2d 
 |-  ( ( ( R Or A /\ A e. Fin ) /\ f e. NN ) -> ( f e. ( `' < " { ( ( # ` A ) + 1 ) } ) <-> ( # ` A ) e. ( ZZ>= ` f ) ) )
35 34 pm5.32da 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( f e. NN /\ f e. ( `' < " { ( ( # ` A ) + 1 ) } ) ) <-> ( f e. NN /\ ( # ` A ) e. ( ZZ>= ` f ) ) ) )
36 2 elin2 
 |-  ( f e. B <-> ( f e. NN /\ f e. ( `' < " { ( ( # ` A ) + 1 ) } ) ) )
37 elfzuzb 
 |-  ( f e. ( 1 ... ( # ` A ) ) <-> ( f e. ( ZZ>= ` 1 ) /\ ( # ` A ) e. ( ZZ>= ` f ) ) )
38 elnnuz 
 |-  ( f e. NN <-> f e. ( ZZ>= ` 1 ) )
39 38 anbi1i 
 |-  ( ( f e. NN /\ ( # ` A ) e. ( ZZ>= ` f ) ) <-> ( f e. ( ZZ>= ` 1 ) /\ ( # ` A ) e. ( ZZ>= ` f ) ) )
40 37 39 bitr4i 
 |-  ( f e. ( 1 ... ( # ` A ) ) <-> ( f e. NN /\ ( # ` A ) e. ( ZZ>= ` f ) ) )
41 35 36 40 3bitr4g 
 |-  ( ( R Or A /\ A e. Fin ) -> ( f e. B <-> f e. ( 1 ... ( # ` A ) ) ) )
42 41 eqrdv 
 |-  ( ( R Or A /\ A e. Fin ) -> B = ( 1 ... ( # ` A ) ) )
43 isoeq4 
 |-  ( B = ( 1 ... ( # ` A ) ) -> ( ( `' G |` B ) Isom < , _E ( B , C ) <-> ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , C ) ) )
44 42 43 syl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( `' G |` B ) Isom < , _E ( B , C ) <-> ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , C ) ) )
45 22 44 mpbid 
 |-  ( ( R Or A /\ A e. Fin ) -> ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , C ) )
46 4 oion 
 |-  ( A e. Fin -> dom O e. On )
47 46 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> dom O e. On )
48 simpr 
 |-  ( ( R Or A /\ A e. Fin ) -> A e. Fin )
49 wofi 
 |-  ( ( R Or A /\ A e. Fin ) -> R We A )
50 4 oien 
 |-  ( ( A e. Fin /\ R We A ) -> dom O ~~ A )
51 48 49 50 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> dom O ~~ A )
52 enfii 
 |-  ( ( A e. Fin /\ dom O ~~ A ) -> dom O e. Fin )
53 48 51 52 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> dom O e. Fin )
54 47 53 elind 
 |-  ( ( R Or A /\ A e. Fin ) -> dom O e. ( On i^i Fin ) )
55 onfin2 
 |-  _om = ( On i^i Fin )
56 54 55 eleqtrrdi 
 |-  ( ( R Or A /\ A e. Fin ) -> dom O e. _om )
57 eqid 
 |-  ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) = ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om )
58 0z 
 |-  0 e. ZZ
59 1 57 8 58 uzrdgxfr 
 |-  ( dom O e. _om -> ( G ` dom O ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) + ( 1 - 0 ) ) )
60 1m0e1 
 |-  ( 1 - 0 ) = 1
61 60 oveq2i 
 |-  ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) + ( 1 - 0 ) ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) + 1 )
62 59 61 eqtrdi 
 |-  ( dom O e. _om -> ( G ` dom O ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) + 1 ) )
63 56 62 syl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( G ` dom O ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) + 1 ) )
64 51 ensymd 
 |-  ( ( R Or A /\ A e. Fin ) -> A ~~ dom O )
65 cardennn 
 |-  ( ( A ~~ dom O /\ dom O e. _om ) -> ( card ` A ) = dom O )
66 64 56 65 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> ( card ` A ) = dom O )
67 66 fveq2d 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) )
68 57 hashgval 
 |-  ( A e. Fin -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
69 68 adantl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
70 67 69 eqtr3d 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) = ( # ` A ) )
71 70 oveq1d 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 0 ) |` _om ) ` dom O ) + 1 ) = ( ( # ` A ) + 1 ) )
72 63 71 eqtrd 
 |-  ( ( R Or A /\ A e. Fin ) -> ( G ` dom O ) = ( ( # ` A ) + 1 ) )
73 72 fveq2d 
 |-  ( ( R Or A /\ A e. Fin ) -> ( `' G ` ( G ` dom O ) ) = ( `' G ` ( ( # ` A ) + 1 ) ) )
74 isof1o 
 |-  ( G Isom _E , < ( _om , NN ) -> G : _om -1-1-onto-> NN )
75 12 74 ax-mp 
 |-  G : _om -1-1-onto-> NN
76 f1ocnvfv1 
 |-  ( ( G : _om -1-1-onto-> NN /\ dom O e. _om ) -> ( `' G ` ( G ` dom O ) ) = dom O )
77 75 56 76 sylancr 
 |-  ( ( R Or A /\ A e. Fin ) -> ( `' G ` ( G ` dom O ) ) = dom O )
78 73 77 eqtr3d 
 |-  ( ( R Or A /\ A e. Fin ) -> ( `' G ` ( ( # ` A ) + 1 ) ) = dom O )
79 78 ineq2d 
 |-  ( ( R Or A /\ A e. Fin ) -> ( _om i^i ( `' G ` ( ( # ` A ) + 1 ) ) ) = ( _om i^i dom O ) )
80 ordom 
 |-  Ord _om
81 ordelss 
 |-  ( ( Ord _om /\ dom O e. _om ) -> dom O C_ _om )
82 80 56 81 sylancr 
 |-  ( ( R Or A /\ A e. Fin ) -> dom O C_ _om )
83 sseqin2 
 |-  ( dom O C_ _om <-> ( _om i^i dom O ) = dom O )
84 82 83 sylib 
 |-  ( ( R Or A /\ A e. Fin ) -> ( _om i^i dom O ) = dom O )
85 79 84 eqtrd 
 |-  ( ( R Or A /\ A e. Fin ) -> ( _om i^i ( `' G ` ( ( # ` A ) + 1 ) ) ) = dom O )
86 3 85 eqtrid 
 |-  ( ( R Or A /\ A e. Fin ) -> C = dom O )
87 isoeq5 
 |-  ( C = dom O -> ( ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , C ) <-> ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , dom O ) ) )
88 86 87 syl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , C ) <-> ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , dom O ) ) )
89 45 88 mpbid 
 |-  ( ( R Or A /\ A e. Fin ) -> ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , dom O ) )
90 4 oiiso 
 |-  ( ( A e. Fin /\ R We A ) -> O Isom _E , R ( dom O , A ) )
91 48 49 90 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> O Isom _E , R ( dom O , A ) )
92 isotr 
 |-  ( ( ( `' G |` B ) Isom < , _E ( ( 1 ... ( # ` A ) ) , dom O ) /\ O Isom _E , R ( dom O , A ) ) -> ( O o. ( `' G |` B ) ) Isom < , R ( ( 1 ... ( # ` A ) ) , A ) )
93 89 91 92 syl2anc 
 |-  ( ( R Or A /\ A e. Fin ) -> ( O o. ( `' G |` B ) ) Isom < , R ( ( 1 ... ( # ` A ) ) , A ) )
94 isof1o 
 |-  ( ( O o. ( `' G |` B ) ) Isom < , R ( ( 1 ... ( # ` A ) ) , A ) -> ( O o. ( `' G |` B ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
95 f1of 
 |-  ( ( O o. ( `' G |` B ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( O o. ( `' G |` B ) ) : ( 1 ... ( # ` A ) ) --> A )
96 93 94 95 3syl 
 |-  ( ( R Or A /\ A e. Fin ) -> ( O o. ( `' G |` B ) ) : ( 1 ... ( # ` A ) ) --> A )
97 fzfid 
 |-  ( ( R Or A /\ A e. Fin ) -> ( 1 ... ( # ` A ) ) e. Fin )
98 96 97 fexd 
 |-  ( ( R Or A /\ A e. Fin ) -> ( O o. ( `' G |` B ) ) e. _V )
99 isoeq1 
 |-  ( f = ( O o. ( `' G |` B ) ) -> ( f Isom < , R ( ( 1 ... ( # ` A ) ) , A ) <-> ( O o. ( `' G |` B ) ) Isom < , R ( ( 1 ... ( # ` A ) ) , A ) ) )
100 98 93 99 spcedv 
 |-  ( ( R Or A /\ A e. Fin ) -> E. f f Isom < , R ( ( 1 ... ( # ` A ) ) , A ) )