Metamath Proof Explorer


Theorem fz1isolem

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

Ref Expression
Hypotheses fz1iso.1 G=recnVn+11ω
fz1iso.2 B=<-1A+1
fz1iso.3 C=ωG-1A+1
fz1iso.4 O=OrdIsoRA
Assertion fz1isolem ROrAAFinffIsom<,R1AA

Proof

Step Hyp Ref Expression
1 fz1iso.1 G=recnVn+11ω
2 fz1iso.2 B=<-1A+1
3 fz1iso.3 C=ωG-1A+1
4 fz1iso.4 O=OrdIsoRA
5 hashcl AFinA0
6 5 adantl ROrAAFinA0
7 nnuz =1
8 1z 1
9 8 1 om2uzisoi GIsomE,<ω1
10 isoeq5 =1GIsomE,<ωGIsomE,<ω1
11 9 10 mpbiri =1GIsomE,<ω
12 7 11 ax-mp GIsomE,<ω
13 isocnv GIsomE,<ωG-1Isom<,Eω
14 12 13 ax-mp G-1Isom<,Eω
15 nn0p1nn A0A+1
16 fvex G-1A+1V
17 16 epini E-1G-1A+1=G-1A+1
18 17 ineq2i ωE-1G-1A+1=ωG-1A+1
19 3 18 eqtr4i C=ωE-1G-1A+1
20 2 19 isoini2 G-1Isom<,EωA+1G-1BIsom<,EBC
21 14 15 20 sylancr A0G-1BIsom<,EBC
22 6 21 syl ROrAAFinG-1BIsom<,EBC
23 nnz ff
24 6 nn0zd ROrAAFinA
25 eluz fAAffA
26 23 24 25 syl2anr ROrAAFinfAffA
27 zleltp1 fAfAf<A+1
28 23 24 27 syl2anr ROrAAFinffAf<A+1
29 ovex A+1V
30 vex fV
31 30 eliniseg A+1Vf<-1A+1f<A+1
32 29 31 ax-mp f<-1A+1f<A+1
33 28 32 bitr4di ROrAAFinffAf<-1A+1
34 26 33 bitr2d ROrAAFinff<-1A+1Af
35 34 pm5.32da ROrAAFinff<-1A+1fAf
36 2 elin2 fBff<-1A+1
37 elfzuzb f1Af1Af
38 elnnuz ff1
39 38 anbi1i fAff1Af
40 37 39 bitr4i f1AfAf
41 35 36 40 3bitr4g ROrAAFinfBf1A
42 41 eqrdv ROrAAFinB=1A
43 isoeq4 B=1AG-1BIsom<,EBCG-1BIsom<,E1AC
44 42 43 syl ROrAAFinG-1BIsom<,EBCG-1BIsom<,E1AC
45 22 44 mpbid ROrAAFinG-1BIsom<,E1AC
46 4 oion AFindomOOn
47 46 adantl ROrAAFindomOOn
48 simpr ROrAAFinAFin
49 wofi ROrAAFinRWeA
50 4 oien AFinRWeAdomOA
51 48 49 50 syl2anc ROrAAFindomOA
52 enfii AFindomOAdomOFin
53 48 51 52 syl2anc ROrAAFindomOFin
54 47 53 elind ROrAAFindomOOnFin
55 onfin2 ω=OnFin
56 54 55 eleqtrrdi ROrAAFindomOω
57 eqid recnVn+10ω=recnVn+10ω
58 0z 0
59 1 57 8 58 uzrdgxfr domOωGdomO=recnVn+10ωdomO+1-0
60 1m0e1 10=1
61 60 oveq2i recnVn+10ωdomO+1-0=recnVn+10ωdomO+1
62 59 61 eqtrdi domOωGdomO=recnVn+10ωdomO+1
63 56 62 syl ROrAAFinGdomO=recnVn+10ωdomO+1
64 51 ensymd ROrAAFinAdomO
65 cardennn AdomOdomOωcardA=domO
66 64 56 65 syl2anc ROrAAFincardA=domO
67 66 fveq2d ROrAAFinrecnVn+10ωcardA=recnVn+10ωdomO
68 57 hashgval AFinrecnVn+10ωcardA=A
69 68 adantl ROrAAFinrecnVn+10ωcardA=A
70 67 69 eqtr3d ROrAAFinrecnVn+10ωdomO=A
71 70 oveq1d ROrAAFinrecnVn+10ωdomO+1=A+1
72 63 71 eqtrd ROrAAFinGdomO=A+1
73 72 fveq2d ROrAAFinG-1GdomO=G-1A+1
74 isof1o GIsomE,<ωG:ω1-1 onto
75 12 74 ax-mp G:ω1-1 onto
76 f1ocnvfv1 G:ω1-1 ontodomOωG-1GdomO=domO
77 75 56 76 sylancr ROrAAFinG-1GdomO=domO
78 73 77 eqtr3d ROrAAFinG-1A+1=domO
79 78 ineq2d ROrAAFinωG-1A+1=ωdomO
80 ordom Ordω
81 ordelss OrdωdomOωdomOω
82 80 56 81 sylancr ROrAAFindomOω
83 sseqin2 domOωωdomO=domO
84 82 83 sylib ROrAAFinωdomO=domO
85 79 84 eqtrd ROrAAFinωG-1A+1=domO
86 3 85 eqtrid ROrAAFinC=domO
87 isoeq5 C=domOG-1BIsom<,E1ACG-1BIsom<,E1AdomO
88 86 87 syl ROrAAFinG-1BIsom<,E1ACG-1BIsom<,E1AdomO
89 45 88 mpbid ROrAAFinG-1BIsom<,E1AdomO
90 4 oiiso AFinRWeAOIsomE,RdomOA
91 48 49 90 syl2anc ROrAAFinOIsomE,RdomOA
92 isotr G-1BIsom<,E1AdomOOIsomE,RdomOAOG-1BIsom<,R1AA
93 89 91 92 syl2anc ROrAAFinOG-1BIsom<,R1AA
94 isof1o OG-1BIsom<,R1AAOG-1B:1A1-1 ontoA
95 f1of OG-1B:1A1-1 ontoAOG-1B:1AA
96 93 94 95 3syl ROrAAFinOG-1B:1AA
97 fzfid ROrAAFin1AFin
98 96 97 fexd ROrAAFinOG-1BV
99 isoeq1 f=OG-1BfIsom<,R1AAOG-1BIsom<,R1AA
100 98 93 99 spcedv ROrAAFinffIsom<,R1AA