Metamath Proof Explorer


Theorem unbenlem

Description: Lemma for unben . (Contributed by NM, 5-May-2005) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis unbenlem.1 G = rec x V x + 1 1 ω
Assertion unbenlem A m n A m < n A ω

Proof

Step Hyp Ref Expression
1 unbenlem.1 G = rec x V x + 1 1 ω
2 nnex V
3 2 ssex A A V
4 1z 1
5 4 1 om2uzf1oi G : ω 1-1 onto 1
6 nnuz = 1
7 f1oeq3 = 1 G : ω 1-1 onto G : ω 1-1 onto 1
8 6 7 ax-mp G : ω 1-1 onto G : ω 1-1 onto 1
9 5 8 mpbir G : ω 1-1 onto
10 f1ocnv G : ω 1-1 onto G -1 : 1-1 onto ω
11 f1of1 G -1 : 1-1 onto ω G -1 : 1-1 ω
12 9 10 11 mp2b G -1 : 1-1 ω
13 f1ores G -1 : 1-1 ω A G -1 A : A 1-1 onto G -1 A
14 12 13 mpan A G -1 A : A 1-1 onto G -1 A
15 f1oeng A V G -1 A : A 1-1 onto G -1 A A G -1 A
16 3 14 15 syl2anc A A G -1 A
17 16 adantr A m n A m < n A G -1 A
18 imassrn G -1 A ran G -1
19 dfdm4 dom G = ran G -1
20 f1of G : ω 1-1 onto G : ω
21 9 20 ax-mp G : ω
22 21 fdmi dom G = ω
23 19 22 eqtr3i ran G -1 = ω
24 18 23 sseqtri G -1 A ω
25 4 1 om2uzuzi y ω G y 1
26 25 6 eleqtrrdi y ω G y
27 breq1 m = G y m < n G y < n
28 27 rexbidv m = G y n A m < n n A G y < n
29 28 rspcv G y m n A m < n n A G y < n
30 26 29 syl y ω m n A m < n n A G y < n
31 30 adantr y ω A m n A m < n n A G y < n
32 f1ocnv G -1 A : A 1-1 onto G -1 A G -1 A -1 : G -1 A 1-1 onto A
33 14 32 syl A G -1 A -1 : G -1 A 1-1 onto A
34 f1ofun G : ω 1-1 onto Fun G
35 9 34 ax-mp Fun G
36 funcnvres2 Fun G G -1 A -1 = G G -1 A
37 f1oeq1 G -1 A -1 = G G -1 A G -1 A -1 : G -1 A 1-1 onto A G G -1 A : G -1 A 1-1 onto A
38 35 36 37 mp2b G -1 A -1 : G -1 A 1-1 onto A G G -1 A : G -1 A 1-1 onto A
39 33 38 sylib A G G -1 A : G -1 A 1-1 onto A
40 f1ofo G G -1 A : G -1 A 1-1 onto A G G -1 A : G -1 A onto A
41 forn G G -1 A : G -1 A onto A ran G G -1 A = A
42 40 41 syl G G -1 A : G -1 A 1-1 onto A ran G G -1 A = A
43 42 eleq2d G G -1 A : G -1 A 1-1 onto A n ran G G -1 A n A
44 f1ofn G G -1 A : G -1 A 1-1 onto A G G -1 A Fn G -1 A
45 fvelrnb G G -1 A Fn G -1 A n ran G G -1 A m G -1 A G G -1 A m = n
46 44 45 syl G G -1 A : G -1 A 1-1 onto A n ran G G -1 A m G -1 A G G -1 A m = n
47 43 46 bitr3d G G -1 A : G -1 A 1-1 onto A n A m G -1 A G G -1 A m = n
48 39 47 syl A n A m G -1 A G G -1 A m = n
49 48 biimpa A n A m G -1 A G G -1 A m = n
50 fvres m G -1 A G G -1 A m = G m
51 50 eqeq1d m G -1 A G G -1 A m = n G m = n
52 51 biimpa m G -1 A G G -1 A m = n G m = n
53 52 adantll y ω m G -1 A G G -1 A m = n G m = n
54 24 sseli m G -1 A m ω
55 4 1 om2uzlt2i y ω m ω y m G y < G m
56 54 55 sylan2 y ω m G -1 A y m G y < G m
57 breq2 G m = n G y < G m G y < n
58 56 57 sylan9bb y ω m G -1 A G m = n y m G y < n
59 53 58 syldan y ω m G -1 A G G -1 A m = n y m G y < n
60 59 biimparc G y < n y ω m G -1 A G G -1 A m = n y m
61 60 exp44 G y < n y ω m G -1 A G G -1 A m = n y m
62 61 imp31 G y < n y ω m G -1 A G G -1 A m = n y m
63 62 reximdva G y < n y ω m G -1 A G G -1 A m = n m G -1 A y m
64 49 63 syl5 G y < n y ω A n A m G -1 A y m
65 64 exp4b G y < n y ω A n A m G -1 A y m
66 65 com4l y ω A n A G y < n m G -1 A y m
67 66 imp y ω A n A G y < n m G -1 A y m
68 67 rexlimdv y ω A n A G y < n m G -1 A y m
69 31 68 syld y ω A m n A m < n m G -1 A y m
70 69 ex y ω A m n A m < n m G -1 A y m
71 70 com3l A m n A m < n y ω m G -1 A y m
72 71 imp A m n A m < n y ω m G -1 A y m
73 72 ralrimiv A m n A m < n y ω m G -1 A y m
74 unbnn3 G -1 A ω y ω m G -1 A y m G -1 A ω
75 24 73 74 sylancr A m n A m < n G -1 A ω
76 entr A G -1 A G -1 A ω A ω
77 17 75 76 syl2anc A m n A m < n A ω