Theorem unbenlem 7504

Description: Lemma for unben 7505.

Hypothesis

Ref	Expression
unbenlem.1	|- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)

Assertion

Ref	Expression
unbenlem	|- ((A (_ NN /\ A.m e. NN E.n e. A m < n) -> A ~~ om)

Distinct variable groups:   m,n,z,w,A   m,G,n

Proof of Theorem unbenlem

Step	Hyp	Ref	Expression
1		entrt 4414	. 2 |- ((A ~~ (`'G"A) /\ (`'G"A) ~~ om) -> A ~~ om)
2		f1oeng 4395	. . . 4 |- ((A e. V /\ (`'G |` A):A-1-1-onto->(`'G"A)) -> A ~~ (`'G"A))
3		nnex 5933	. . . . 5 |- NN e. V
4	3	ssex 2719	. . . 4 |- (A (_ NN -> A e. V)
5		1z 6159	. . . . . . . . 9 |- 1 e. ZZ
6		unbenlem.1	. . . . . . . . 9 |- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
7	5, 6	om2uzf1o 6301	. . . . . . . 8 |- G:om-1-1-onto->{t e. ZZ | 1 <_ t}
8		nnzrab 6157	. . . . . . . . 9 |- NN = {t e. ZZ | 1 <_ t}
9		f1oeq3 3686	. . . . . . . . 9 |- (NN = {t e. ZZ | 1 <_ t} -> (G:om-1-1-onto->NN <-> G:om-1-1-onto->{t e. ZZ | 1 <_ t}))
10	8, 9	ax-mp 7	. . . . . . . 8 |- (G:om-1-1-onto->NN <-> G:om-1-1-onto->{t e. ZZ | 1 <_ t})
11	7, 10	mpbir 190	. . . . . . 7 |- G:om-1-1-onto->NN
12		f1ocnv 3701	. . . . . . 7 |- (G:om-1-1-onto->NN -> `'G:NN-1-1-onto->om)
13	11, 12	ax-mp 7	. . . . . 6 |- `'G:NN-1-1-onto->om
14		f1of1 3688	. . . . . 6 |- (`'G:NN-1-1-onto->om -> `'G:NN-1-1->om)
15	13, 14	ax-mp 7	. . . . 5 |- `'G:NN-1-1->om
16		f1ores 3703	. . . . 5 |- ((`'G:NN-1-1->om /\ A (_ NN) -> (`'G |` A):A-1-1-onto->(`'G"A))
17	15, 16	mpan 695	. . . 4 |- (A (_ NN -> (`'G |` A):A-1-1-onto->(`'G"A))
18	2, 4, 17	sylanc 471	. . 3 |- (A (_ NN -> A ~~ (`'G"A))
19	18	adantr 389	. 2 |- ((A (_ NN /\ A.m e. NN E.n e. A m < n) -> A ~~ (`'G"A))
20	5, 6	om2uzuz 6297	. . . . . . . . . . . 12 |- (v e. om -> (G` v) e. {t e. ZZ | 1 <_ t})
21	20, 8	syl6eleqr 1559	. . . . . . . . . . 11 |- (v e. om -> (G` v) e. NN)
22		breq1 2622	. . . . . . . . . . . . 13 |- (m = (G` v) -> (m < n <-> (G` v) < n))
23	22	rexbidv 1664	. . . . . . . . . . . 12 |- (m = (G` v) -> (E.n e. A m < n <-> E.n e. A (G` v) < n))
24	23	rcla4v 1873	. . . . . . . . . . 11 |- ((G` v) e. NN -> (A.m e. NN E.n e. A m < n -> E.n e. A (G` v) < n))
25	21, 24	syl 10	. . . . . . . . . 10 |- (v e. om -> (A.m e. NN E.n e. A m < n -> E.n e. A (G` v) < n))
26	25	adantr 389	. . . . . . . . 9 |- ((v e. om /\ A (_ NN) -> (A.m e. NN E.n e. A m < n -> E.n e. A (G` v) < n))
27		fvres 3734	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. (`'G"A) -> ((G |` (`'G"A))` u) = (G` u))
28	27	eqeq1d 1483	. . . . . . . . . . . . . . . . . . . . 21 |- (u e. (`'G"A) -> (((G |` (`'G"A))` u) = n <-> (G` u) = n))
29	28	biimpa 416	. . . . . . . . . . . . . . . . . . . 20 |- ((u e. (`'G"A) /\ ((G |` (`'G"A))` u) = n) -> (G` u) = n)
30	29	adantll 392	. . . . . . . . . . . . . . . . . . 19 |- (((v e. om /\ u e. (`'G"A)) /\ ((G |` (`'G"A))` u) = n) -> (G` u) = n)
31	5, 6	om2uzlt2 6299	. . . . . . . . . . . . . . . . . . . . 21 |- ((v e. om /\ u e. om) -> (v e. u <-> (G` v) < (G` u)))
32		imassrn 3415	. . . . . . . . . . . . . . . . . . . . . . 23 |- (`'G"A) (_ ran `' G
33		dfdm4 3305	. . . . . . . . . . . . . . . . . . . . . . . 24 |- dom G = ran `' G
34		f1of 3689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (G:om-1-1-onto->NN -> G:om-->NN)
35	11, 34	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- G:om-->NN
36	35	fdmi 3632	. . . . . . . . . . . . . . . . . . . . . . . 24 |- dom G = om
37	33, 36	eqtr3 1497	. . . . . . . . . . . . . . . . . . . . . . 23 |- ran `' G = om
38	32, 37	sseqtr 2093	. . . . . . . . . . . . . . . . . . . . . 22 |- (`'G"A) (_ om
39	38	sseli 2065	. . . . . . . . . . . . . . . . . . . . 21 |- (u e. (`'G"A) -> u e. om)
40	31, 39	sylan2 451	. . . . . . . . . . . . . . . . . . . 20 |- ((v e. om /\ u e. (`'G"A)) -> (v e. u <-> (G` v) < (G` u)))
41		breq2 2623	. . . . . . . . . . . . . . . . . . . 20 |- ((G` u) = n -> ((G` v) < (G` u) <-> (G` v) < n))
42	40, 41	sylan9bb 540	. . . . . . . . . . . . . . . . . . 19 |- (((v e. om /\ u e. (`'G"A)) /\ (G` u) = n) -> (v e. u <-> (G` v) < n))
43	30, 42	syldan 467	. . . . . . . . . . . . . . . . . 18 |- (((v e. om /\ u e. (`'G"A)) /\ ((G |` (`'G"A))` u) = n) -> (v e. u <-> (G` v) < n))
44	43	biimparc 419	. . . . . . . . . . . . . . . . 17 |- (((G` v) < n /\ ((v e. om /\ u e. (`'G"A)) /\ ((G |` (`'G"A))` u) = n)) -> v e. u)
45	44	exp44 385	. . . . . . . . . . . . . . . 16 |- ((G` v) < n -> (v e. om -> (u e. (`'G"A) -> (((G |` (`'G"A))` u) = n -> v e. u))))
46	45	imp31 362	. . . . . . . . . . . . . . 15 |- ((((G` v) < n /\ v e. om) /\ u e. (`'G"A)) -> (((G |` (`'G"A))` u) = n -> v e. u))
47	46	r19.22dva 1739	. . . . . . . . . . . . . 14 |- (((G` v) < n /\ v e. om) -> (E.u e. (`'G"A)((G |` (`'G"A))` u) = n -> E.u e. (`'G"A)v e. u))
48		f1ocnv 3701	. . . . . . . . . . . . . . . . . 18 |- ((`'G |` A):A-1-1-onto->(`'G"A) -> `'(`'G |` A):(`'G"A)-1-1-onto->A)
49	17, 48	syl 10	. . . . . . . . . . . . . . . . 17 |- (A (_ NN -> `'(`'G |` A):(`'G"A)-1-1-onto->A)
50		f1ofun 3691	. . . . . . . . . . . . . . . . . . . 20 |- (G:om-1-1-onto->NN -> Fun G)
51	11, 50	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- Fun G
52		funcnvres2 3570	. . . . . . . . . . . . . . . . . . 19 |- (Fun G -> `'(`'G |` A) = (G |` (`'G"A)))
53	51, 52	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- `'(`'G |` A) = (G |` (`'G"A))
54		f1oeq1 3684	. . . . . . . . . . . . . . . . . 18 |- (`'(`'G |` A) = (G |` (`'G"A)) -> (`'(`'G |` A):(`'G"A)-1-1-onto->A <-> (G |` (`'G"A)):(`'G"A)-1-1-onto->A))
55	53, 54	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (`'(`'G |` A):(`'G"A)-1-1-onto->A <-> (G |` (`'G"A)):(`'G"A)-1-1-onto->A)
56	49, 55	sylib 198	. . . . . . . . . . . . . . . 16 |- (A (_ NN -> (G |` (`'G"A)):(`'G"A)-1-1-onto->A)
57		f1ofo 3695	. . . . . . . . . . . . . . . . . . 19 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (G |` (`'G"A)):(`'G"A)-onto->A)
58		forn 3674	. . . . . . . . . . . . . . . . . . 19 |- ((G |` (`'G"A)):(`'G"A)-onto->A -> ran ( G |` (`'G"A)) = A)
59	57, 58	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> ran ( G |` (`'G"A)) = A)
60	59	eleq2d 1541	. . . . . . . . . . . . . . . . 17 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (n e. ran ( G |` (`'G"A)) <-> n e. A))
61		f1ofn 3690	. . . . . . . . . . . . . . . . . 18 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (G |` (`'G"A)) Fn (`'G"A))
62		fvelrnb 3760	. . . . . . . . . . . . . . . . . 18 |- ((G |` (`'G"A)) Fn (`'G"A) -> (n e. ran ( G |` (`'G"A)) <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
63	61, 62	syl 10	. . . . . . . . . . . . . . . . 17 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (n e. ran ( G |` (`'G"A)) <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
64	60, 63	bitr3d 530	. . . . . . . . . . . . . . . 16 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (n e. A <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
65	56, 64	syl 10	. . . . . . . . . . . . . . 15 |- (A (_ NN -> (n e. A <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
66	65	biimpa 416	. . . . . . . . . . . . . 14 |- ((A (_ NN /\ n e. A) -> E.u e. (`'G"A)((G |` (`'G"A))` u) = n)
67	47, 66	syl5 21	. . . . . . . . . . . . 13 |- (((G` v) < n /\ v e. om) -> ((A (_ NN /\ n e.