Theorem om2uzlt 4654

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

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(s):   x,y,C

Proof of Theorem om2uzlt

Step	Hyp	Ref	Expression
1		eleq2 1150	. . . . . 6 |- (v = (/) -> (A e. v <-> A e. (/)))
2		fveq2 2832	. . . . . . 7 |- (v = (/) -> (G` v) = (G` (/)))
3	2	breq2d 2072	. . . . . 6 |- (v = (/) -> ((G` A) < (G` v) <-> (G` A) < (G` (/))))
4	1, 3	imbi12d 474	. . . . 5 |- (v = (/) -> ((A e. v -> (G` A) < (G` v)) <-> (A e. (/) -> (G` A) < (G` (/)))))
5	4	imbi2d 464	. . . 4 |- (v = (/) -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. (/) -> (G` A) < (G` (/))))))
6		eleq2 1150	. . . . . 6 |- (v = w -> (A e. v <-> A e. w))
7		fveq2 2832	. . . . . . 7 |- (v = w -> (G` v) = (G` w))
8	7	breq2d 2072	. . . . . 6 |- (v = w -> ((G` A) < (G` v) <-> (G` A) < (G` w)))
9	6, 8	imbi12d 474	. . . . 5 |- (v = w -> ((A e. v -> (G` A) < (G` v)) <-> (A e. w -> (G` A) < (G` w))))
10	9	imbi2d 464	. . . 4 |- (v = w -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. w -> (G` A) < (G` w)))))
11		eleq2 1150	. . . . . 6 |- (v = suc w -> (A e. v <-> A e. suc w))
12		fveq2 2832	. . . . . . 7 |- (v = suc w -> (G` v) = (G` suc w))
13	12	breq2d 2072	. . . . . 6 |- (v = suc w -> ((G` A) < (G` v) <-> (G` A) < (G` suc w)))
14	11, 13	imbi12d 474	. . . . 5 |- (v = suc w -> ((A e. v -> (G` A) < (G` v)) <-> (A e. suc w -> (G` A) < (G` suc w))))
15	14	imbi2d 464	. . . 4 |- (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 1150	. . . . . 6 |- (v = B -> (A e. v <-> A e. B))
17		fveq2 2832	. . . . . . 7 |- (v = B -> (G` v) = (G` B))
18	17	breq2d 2072	. . . . . 6 |- (v = B -> ((G` A) < (G` v) <-> (G` A) < (G` B)))
19	16, 18	imbi12d 474	. . . . 5 |- (v = B -> ((A e. v -> (G` A) < (G` v)) <-> (A e. B -> (G` A) < (G` B))))
20	19	imbi2d 464	. . . 4 |- (v = B -> ((A e. om -> (A e. v -> (G` A) < (G` v))) <-> (A e. om -> (A e. B -> (G` A) < (G` B)))))
21		noel 1711	. . . . . 6 |- -. A e. (/)
22	21	pm2.21i 73	. . . . 5 |- (A e. (/) -> (G` A) < (G` (/)))
23	22	a1i 7	. . . 4 |- (A e. om -> (A e. (/) -> (G` A) < (G` (/))))
24		elsuc2g 2291	. . . . . . . . . . 11 |- (w e. om -> (A e. suc w <-> (A e. w \/ A = w)))
25	24	bicomd 399	. . . . . . . . . 10 |- (w e. om -> ((A e. w \/ A = w) <-> A e. suc w))
26	25	adantl 305	. . . . . . . . 9 |- ((A e. om /\ w e. om) -> ((A e. w \/ A = w) <-> A e. suc w))
27		leloet 4284	. . . . . . . . . . 11 |- (((G` A) e. RR /\ (G` w) e. RR) -> ((G` A) <_ (G` w) <-> ((G` A) < (G` w) \/ (G` A) = (G` w))))
28		om2uz.1	. . . . . . . . . . . . 13 |- C e. ZZ
29		om2uz.2	. . . . . . . . . . . . 13 |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)
30	28, 29	om2uzuz 4653	. . . . . . . . . . . 12 |- (A e. om -> (G` A) e. {z e. ZZ | C <_ z})
31		ssrab 1556	. . . . . . . . . . . . 13 |- {z e. ZZ | C <_ z} (_ ZZ
32	31	sseli 1504	. . . . . . . . . . . 12 |- ((G` A) e. {z e. ZZ | C <_ z} -> (G` A) e. ZZ)
33		zret 4567	. . . . . . . . . . . 12 |- ((G` A) e. ZZ -> (G` A) e. RR)
34	30, 32, 33	3syl 21	. . . . . . . . . . 11 |- (A e. om -> (G` A) e. RR)
35	28, 29	om2uzuz 4653	. . . . . . . . . . . 12 |- (w e. om -> (G` w) e. {z e. ZZ | C <_ z})
36	31	sseli 1504	. . . . . . . . . . . 12 |- ((G` w) e. {z e. ZZ | C <_ z} -> (G` w) e. ZZ)
37		zret 4567	. . . . . . . . . . . 12 |- ((G` w) e. ZZ -> (G` w) e. RR)
38	35, 36, 37	3syl 21	. . . . . . . . . . 11 |- (w e. om -> (G` w) e. RR)
39	27, 34, 38	syl2an 349	. . . . . . . . . 10 |- ((A e. om /\ w e. om) -> ((G` A) <_ (G` w) <-> ((G` A) < (G` w) \/ (G` A) = (G` w))))
40		zleltp1t 4598	. . . . . . . . . . . . 13 |- (((G` A) e. ZZ /\ (G` w) e. ZZ) -> ((G` A) <_ (G` w) <-> (G` A) < ((G` w) + 1)))
41	40, 32, 36	syl2an 349	. . . . . . . . . . . 12 |- (((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)))
42	41, 30, 35	syl2an 349	. . . . . . . . . . 11 |- ((A e. om /\ w e. om) -> ((G` A) <_ (G` w) <-> (G` A) < ((G` w) + 1)))
43	28, 29	om2uzsuc 4652	. . . . . . . . . . . . 13 |- (w e. om -> (G` suc w) = ((G` w) + 1))
44	43	breq2d 2072	. . . . . . . . . . . 12 |- (w e. om -> ((G` A) < (G` suc w) <-> (G` A) < ((G` w) + 1)))
45	44	adantl 305	. . . . . . . . . . 11 |- ((A e. om /\ w e. om) -> ((G` A) < (G` suc w) <-> (G` A) < ((G` w) + 1)))
46	42, 45	bitr4d 409	. . . . . . . . . 10 |- ((A e. om /\ w e. om) -> ((G` A) <_ (G` w) <-> (G` A) < (G` suc w)))
47	39, 46	bitr3d 408	. . . . . . . . 9 |- ((A e. om /\ w e. om) -> (((G` A) < (G` w) \/ (G` A) = (G` w)) <-> (G` A) < (G` suc w)))
48	26, 47	imbi12d 474	. . . . . . . 8 |- ((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))))
49		id 9	. . . . . . . . 9 |- ((A e. w -> (G` A) < (G` w)) -> (A e. w -> (G` A) < (G` w)))
50		fveq2 2832	. . . . . . . . . 10 |- (A = w -> (G` A) = (G` w))
51	50	a1i 7	. . . . . . . . 9 |- ((A e. w -> (G` A) < (G` w)) -> (A = w -> (G` A) = (G` w)))
52	49, 51	orim12d 436	. . . . . . . 8 |- ((A e. w -> (G` A) < (G` w)) -> ((A e. w \/ A = w) -> ((G` A) < (G` w) \/ (G` A) = (G` w))))
53	48, 52	syl5bi 183	. . . . . . 7 |- ((A e. om /\ w e. om) -> ((A e. w -> (G` A) < (G` w)) -> (A e. suc w -> (G` A) < (G` suc w))))
54	53	exp 291	. . . . . 6 |- (A e. om -> (w e. om -> ((A e. w -> (G` A) < (G` w)) -> (A e. suc w -> (G` A) < (G` suc w)))))
55	54	com12 13	. . . . 5 |- (w e. om -> (A e. om -> ((A e. w -> (G` A) < (G` w)) -> (A e. suc w -> (G` A) < (G` suc w)))))
56	55	a2d 15	. . . 4 |- (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)))))
57	5, 10, 15, 20, 23, 56	finds 2397	. . 3 |- (B e. om -> (A e. om -> (A e. B -> (G` A) < (G` B))))
58	57	com12 13	. 2 |- (A e. om -> (B e. om -> (A e. B -> (G` A) < (G` B))))
59	58	imp 277	1 |- ((A e. om /\ B e. om) -> (A e. B -> (G` A) < (G` B)))

Syntax hints: