Theorem om2uzlt 6235

Description: Less-than relation for G (see om2uz0 6232).

Hypotheses

Ref	Expression
om2uz.1	|- C e. ZZ
om2uz.2	|- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)

Assertion

Ref	Expression
om2uzlt	|- ((A e. om /\ B e. om) -> (A e. B -> (G` A) < (G` B)))

Distinct variable group:   x,y,C

Proof of Theorem om2uzlt

Step	Hyp	Ref	Expression
1		eleq2 1527	. . . . 5 |- (v = (/) -> (A e. v <-> A e. (/)))
2		fveq2 3709	. . . . . 6 |- (v = (/) -> (G` v) = (G` (/)))
3	2	breq2d 2620	. . . . 5 |- (v = (/) -> ((G` A) < (G` v) <-> (G` A) < (G` (/))))
4	1, 3	imbi12d 624	. . . 4 |- (v = (/) -> ((A e. v -> (G` A) < (G` v)) <-> (A e. (/) -> (G` A) < (G` (/)))))
5	4	imbi2d 610	. . 3 |- (v = (/) -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. (/) -> (G` A) < (G` (/))))))
6		eleq2 1527	. . . . 5 |- (v = w -> (A e. v <-> A e. w))
7		fveq2 3709	. . . . . 6 |- (v = w -> (G` v) = (G` w))
8	7	breq2d 2620	. . . . 5 |- (v = w -> ((G` A) < (G` v) <-> (G` A) < (G` w)))
9	6, 8	imbi12d 624	. . . 4 |- (v = w -> ((A e. v -> (G` A) < (G` v)) <-> (A e. w -> (G` A) < (G` w))))
10	9	imbi2d 610	. . 3 |- (v = w -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. w -> (G` A) < (G` w)))))
11		eleq2 1527	. . . . 5 |- (v = suc w -> (A e. v <-> A e. suc w))
12		fveq2 3709	. . . . . 6 |- (v = suc w -> (G` v) = (G` suc w))
13	12	breq2d 2620	. . . . 5 |- (v = suc w -> ((G` A) < (G` v) <-> (G` A) < (G` suc w)))
14	11, 13	imbi12d 624	. . . 4 |- (v = suc w -> ((A e. v -> (G` A) < (G` v)) <-> (A e. suc w -> (G` A) < (G` suc w))))
15	14	imbi2d 610	. . 3 |- (v = suc w -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. suc w -> (G` A) < (G` suc w)))))
16		eleq2 1527	. . . . 5 |- (v = B -> (A e. v <-> A e. B))
17		fveq2 3709	. . . . . 6 |- (v = B -> (G` v) = (G` B))
18	17	breq2d 2620	. . . . 5 |- (v = B -> ((G` A) < (G` v) <-> (G` A) < (G` B)))
19	16, 18	imbi12d 624	. . . 4 |- (v = B -> ((A e. v -> (G` A) < (G` v)) <-> (A e. B -> (G` A) < (G` B))))
20	19	imbi2d 610	. . 3 |- (v = B -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. B -> (G` A) < (G` B)))))
21		noel 2274	. . . . 5 |- -. A e. (/)
22	21	pm2.21i 77	. . . 4 |- (A e. (/) -> (G` A) < (G` (/)))
23	22	a1i 8	. . 3 |- (A e. om -> (A e. (/) -> (G` A) < (G` (/))))
24		elsuc2g 3027	. . . . . . . . 9 |- (w e. om -> (A e. suc w <-> (A e. w \/ A = w)))
25	24	bicomd 519	. . . . . . . 8 |- (w e. om -> ((A e. w \/ A = w) <-> A e. suc w))
26	25	adantl 388	. . . . . . 7 |- ((A e. om /\ w e. om) -> ((A e. w \/ A = w) <-> A e. suc w))
27		om2uz.1	. . . . . . . . . . 11 |- C e. ZZ
28		om2uz.2	. . . . . . . . . . 11 |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)
29	27, 28	om2uzsuc 6233	. . . . . . . . . 10 |- (w e. om -> (G` suc w) = ((G` w) + 1))
30	29	breq2d 2620	. . . . . . . . 9 |- (w e. om -> ((G` A) < (G` suc w) <-> (G` A) < ((G` w) + 1)))
31	30	adantl 388	. . . . . . . 8 |- ((A e. om /\ w e. om) -> ((G` A) < (G` suc w) <-> (G` A) < ((G` w) + 1)))
32		zleltp1t 6129	. . . . . . . . . 10 |- (((G` A) e. ZZ /\ (G` w) e. ZZ) -> ((G` A) <_ (G` w) <-> (G` A) < ((G` w) + 1)))
33		ssrab2 2121	. . . . . . . . . . 11 |- {z e. ZZ | C <_ z} (_ ZZ
34	33	sseli 2055	. . . . . . . . . 10 |- ((G` A) e. {z e. ZZ | C <_ z} -> (G` A) e. ZZ)
35	33	sseli 2055	. . . . . . . . . 10 |- ((G` w) e. {z e. ZZ | C <_ z} -> (G` w) e. ZZ)
36	32, 34, 35	syl2an 454	. . . . . . . . 9 |- (((G` A) e. {z e. ZZ | C <_ z} /\ (G` w) e. {z e. ZZ | C <_ z}) -> ((G` A) <_ (G` w) <-> (G` A) < ((G` w) + 1)))
37	27, 28	om2uzuz 6234	. . . . . . . . 9 |- (A e. om -> (G` A) e. {z e. ZZ | C <_ z})
38	27, 28	om2uzuz 6234	. . . . . . . . 9 |- (w e. om -> (G` w) e. {z e. ZZ | C <_ z})
39	36, 37, 38	syl2an 454	. . . . . . . 8 |- ((A e. om /\ w e. om) -> ((G` A) <_ (G` w) <-> (G` A) < ((G` w) + 1)))
40		leloet 5491	. . . . . . . . 9 |- (((G` A) e. RR /\ (G` w) e. RR) -> ((G` A) <_ (G` w) <-> ((G` A) < (G` w) \/ (G` A) = (G` w))))
41		zret 6086	. . . . . . . . . 10 |- ((G` A) e. ZZ -> (G` A) e. RR)
42	37, 34, 41	3syl 20	. . . . . . . . 9 |- (A e. om -> (G` A) e. RR)
43		zret 6086	. . . . . . . . . 10 |- ((G` w) e. ZZ -> (G` w) e. RR)
44	38, 35, 43	3syl 20	. . . . . . . . 9 |- (w e. om -> (G` w) e. RR)
45	40, 42, 44	syl2an 454	. . . . . . . 8 |- ((A e. om /\ w e. om) -> ((G` A) <_ (G` w) <-> ((G` A) < (G` w) \/ (G` A) = (G` w))))
46	31, 39, 45	3bitr2rd 545	. . . . . . 7 |- ((A e. om /\ w e. om) -> (((G` A) < (G` w) \/ (G` A) = (G` w)) <-> (G` A) < (G` suc w)))
47	26, 46	imbi12d 624	. . . . . 6 |- ((A e. om /\ w e. om) -> (((A e. w \/ A = w) -> ((G` A) < (G` w) \/ (G` A) = (G` w))) <-> (A e. suc w -> (G` A) < (G` suc w))))
48		id 59	. . . . . . 7 |- ((A e. w -> (G` A) < (G` w)) -> (A e. w -> (G` A) < (G` w)))
49		fveq2 3709	. . . . . . . 8 |- (A = w -> (G` A) = (G` w))
50	49	a1i 8	. . . . . . 7 |- ((A e. w -> (G` A) < (G` w)) -> (A = w -> (G` A) = (G` w)))
51	48, 50	orim12d 563	. . . . . 6 |- ((A e. w -> (G` A) < (G` w)) -> ((A e. w \/ A = w) -> ((G` A) < (G` w) \/ (G` A) = (G` w))))
52	47, 51	syl5bi 208	. . . . 5 |- ((A e. om /\ w e. om) -> ((A e. w -> (G` A) < (G` w)) -> (A e. suc w -> (G` A) < (G` suc w))))
53	52	expcom 374	. . . 4 |- (w e. om -> (A e. om -> ((A e. w -> (G` A) < (G` w)) -> (A e. suc w -> (G` A) < (G` suc w)))))
54	53	a2d 13	. . 3 |- (w e. om -> ((A e. om -> (A e. w -> (G` A) < (G` w))) -> (A e. om -> (A e. suc w -> (G` A) < (G` suc w)))))
55	5, 10, 15, 20, 23, 54	finds 3146	. 2 |- (B e. om -> (A e. om -> (A e. B -> (G` A) < (G` B))))
56	55	impcom 351	1 |- ((A e. om /\ B e. om) -> (A e. B -> (G` A) < (G` B)))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 953   e. wcel 955  {crab 1640  (/)c0 2270   class class class wbr 2609  {copab 2656  suc csuc 2940  omcom 3121   |` cres 3162  ` cfv 3172  reccrdg 3916  (class class class)co 3948  RRcr 5205  1c1 5207   + caddc 5209   <_ cle 5267  ZZcz 5270   < clt 5458

This theorem is referenced by:  om2uzlt2 6236  om2uzf1o 6238

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963