Theorem unbenlem 7464

Description: Lemma for unben 7465.

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 4404	. 2 |- ((A ~~ (`'G"A) /\ (`'G"A) ~~ om) -> A ~~ om)
2		f1oeng 4385	. . . 4 |- ((A e. V /\ (`'G |` A):A-1-1-onto->(`'G"A)) -> A ~~ (`'G"A))
3		nnex 5891	. . . . 5 |- NN e. V
4	3	ssex 2715	. . . 4 |- (A (_ NN -> A e. V)
5		1z 6116	. . . . . . . . 9 |- 1 e. ZZ
6		unbenlem.1	. . . . . . . . 9 |- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
7	5, 6	om2uzf1o 6251	. . . . . . . 8 |- G:om-1-1-onto->{t e. ZZ | 1 <_ t}
8		nnzrab 6114	. . . . . . . . 9 |- NN = {t e. ZZ | 1 <_ t}
9		f1oeq3 3681	. . . . . . . . 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 3696	. . . . . . 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 3683	. . . . . 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 3698	. . . . 5 |- ((`'G:NN-1-1->om /\ A (_ NN) -> (`'G |` A):A-1-1-onto->(`'G"A))
17	15, 16	mpan 694	. . . 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 6247	. . . . . . . . . . . 12 |- (v e. om -> (G` v) e. {t e. ZZ | 1 <_ t})
21	20, 8	syl6eleqr 1557	. . . . . . . . . . 11 |- (v e. om -> (G` v) e. NN)
22		breq1 2618	. . . . . . . . . . . . 13 |- (m = (G` v) -> (m < n <-> (G` v) < n))
23	22	rexbidv 1662	. . . . . . . . . . . 12 |- (m = (G` v) -> (E.n e. A m < n <-> E.n e. A (G` v) < n))
24	23	rcla4v 1870	. . . . . . . . . . 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 3729	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. (`'G"A) -> ((G |` (`'G"A))` u) = (G` u))
28	27	eqeq1d 1481	. . . . . . . . . . . . . . . . . . . . 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 6249	. . . . . . . . . . . . . . . . . . . . 21 |- ((v e. om /\ u e. om) -> (v e. u <-> (G` v) < (G` u)))
32		imassrn 3411	. . . . . . . . . . . . . . . . . . . . . . 23 |- (`'G"A) (_ ran `' G
33		dfdm4 3301	. . . . . . . . . . . . . . . . . . . . . . . 24 |- dom G = ran `' G
34		f1of 3684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (G:om-1-1-onto->NN -> G:om-->NN)
35	11, 34	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- G:om-->NN
36		fdm 3627	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (G:om-->NN -> dom G = om)
37	35, 36	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24 |- dom G = om
38	33, 37	eqtr3 1495	. . . . . . . . . . . . . . . . . . . . . . 23 |- ran `' G = om
39	32, 38	sseqtr 2090	. . . . . . . . . . . . . . . . . . . . . 22 |- (`'G"A) (_ om
40	39	sseli 2062	. . . . . . . . . . . . . . . . . . . . 21 |- (u e. (`'G"A) -> u e. om)
41	31, 40	sylan2 451	. . . . . . . . . . . . . . . . . . . 20 |- ((v e. om /\ u e. (`'G"A)) -> (v e. u <-> (G` v) < (G` u)))
42		breq2 2619	. . . . . . . . . . . . . . . . . . . 20 |- ((G` u) = n -> ((G` v) < (G` u) <-> (G` v) < n))
43	41, 42	sylan9bb 539	. . . . . . . . . . . . . . . . . . 19 |- (((v e. om /\ u e. (`'G"A)) /\ (G` u) = n) -> (v e. u <-> (G` v) < n))
44	30, 43	syldan 467	. . . . . . . . . . . . . . . . . 18 |- (((v e. om /\ u e. (`'G"A)) /\ ((G |` (`'G"A))` u) = n) -> (v e. u <-> (G` v) < n))
45	44	biimparc 419	. . . . . . . . . . . . . . . . 17 |- (((G` v) < n /\ ((v e. om /\ u e. (`'G"A)) /\ ((G |` (`'G"A))` u) = n)) -> v e. u)
46	45	exp44 385	. . . . . . . . . . . . . . . 16 |- ((G` v) < n -> (v e. om -> (u e. (`'G"A) -> (((G |` (`'G"A))` u) = n -> v e. u))))
47	46	imp31 362	. . . . . . . . . . . . . . 15 |- ((((G` v) < n /\ v e. om) /\ u e. (`'G"A)) -> (((G |` (`'G"A))` u) = n -> v e. u))
48	47	r19.22dva 1737	. . . . . . . . . . . . . 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))
49		f1ocnv 3696	. . . . . . . . . . . . . . . . . 18 |- ((`'G |` A):A-1-1-onto->(`'G"A) -> `'(`'G |` A):(`'G"A)-1-1-onto->A)
50	17, 49	syl 10	. . . . . . . . . . . . . . . . 17 |- (A (_ NN -> `'(`'G |` A):(`'G"A)-1-1-onto->A)
51		f1ofun 3686	. . . . . . . . . . . . . . . . . . . 20 |- (G:om-1-1-onto->NN -> Fun G)
52	11, 51	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- Fun G
53		funcnvres2 3566	. . . . . . . . . . . . . . . . . . 19 |- (Fun G -> `'(`'G |` A) = (G |` (`'G"A)))
54	52, 53	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- `'(`'G |` A) = (G |` (`'G"A))
55		f1oeq1 3679	. . . . . . . . . . . . . . . . . 18 |- (`'(`'G |` A) = (G |` (`'G"A)) -> (`'(`'G |` A):(`'G"A)-1-1-onto->A <-> (G |` (`'G"A)):(`'G"A)-1-1-onto->A))
56	54, 55	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (`'(`'G |` A):(`'G"A)-1-1-onto->A <-> (G |` (`'G"A)):(`'G"A)-1-1-onto->A)
57	50, 56	sylib 198	. . . . . . . . . . . . . . . 16 |- (A (_ NN -> (G |` (`'G"A)):(`'G"A)-1-1-onto->A)
58		f1ofo 3690	. . . . . . . . . . . . . . . . . . 19 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (G |` (`'G"A)):(`'G"A)-onto->A)
59		forn 3669	. . . . . . . . . . . . . . . . . . 19 |- ((G |` (`'G"A)):(`'G"A)-onto->A -> ran ( G |` (`'G"A)) = A)
60	58, 59	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> ran ( G |` (`'G"A)) = A)
61	60	eleq2d 1539	. . . . . . . . . . . . . . . . 17 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (n e. ran ( G |` (`'G"A)) <-> n e. A))
62		f1ofn 3685	. . . . . . . . . . . . . . . . . 18 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (G |` (`'G"A)) Fn (`'G"A))
63		fvelrnb 3755	. . . . . . . . . . . . . . . . . 18 |- ((G |` (`'G"A)) Fn (`'G"A) -> (n e. ran ( G |` (`'G"A)) <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
64	62, 63	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))
65	61, 64	bitr3d 529	. . . . . . . . . . . . . . . 16 |- ((G |` (`'G"A)):(`'G"A)-1-1-onto->A -> (n e. A <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
66	57, 65	syl 10	. . . . . . . . . . . . . . 15 |- (A (_ NN -> (n e. A <-> E.u e. (`'G"A)((G |` (`'G"A))` u) = n))
67	66	biimpa 416	. . . . . . . . . . . . . 14 |- ((A (_ NN /\ n e. A) -> E.u e. (`'G"A)((G |` (`'G"A))` u) = n)
68	48, 67	syl5 21	. . . . . . . . . . . . 13 |- (((G` v