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 e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
Assertion unbenlem 
|- ( ( A C_ NN /\ A. m e. NN E. n e. A m < n ) -> A ~~ _om )

Proof

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