om2uzlti

Description: Less-than relation for G (see om2uz0i ). (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	$⊢ C \in ℤ$
	om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
Assertion	om2uzlti	$⊢ (A \in ω \land B \in ω) \to (A \in B \to G (A) < G (B))$

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	$⊢ C \in ℤ$
2		om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
3		eleq2	$⊢ z = \emptyset \to (A \in z \leftrightarrow A \in \emptyset)$
4		fveq2	$⊢ z = \emptyset \to G (z) = G (\emptyset)$
5	4	breq2d	$⊢ z = \emptyset \to (G (A) < G (z) \leftrightarrow G (A) < G (\emptyset))$
6	3 5	imbi12d	$⊢ z = \emptyset \to ((A \in z \to G (A) < G (z)) \leftrightarrow (A \in \emptyset \to G (A) < G (\emptyset)))$
7	6	imbi2d	$⊢ z = \emptyset \to ((A \in ω \to (A \in z \to G (A) < G (z))) \leftrightarrow (A \in ω \to (A \in \emptyset \to G (A) < G (\emptyset))))$
8		eleq2	$⊢ z = y \to (A \in z \leftrightarrow A \in y)$
9		fveq2	$⊢ z = y \to G (z) = G (y)$
10	9	breq2d	$⊢ z = y \to (G (A) < G (z) \leftrightarrow G (A) < G (y))$
11	8 10	imbi12d	$⊢ z = y \to ((A \in z \to G (A) < G (z)) \leftrightarrow (A \in y \to G (A) < G (y)))$
12	11	imbi2d	$⊢ z = y \to ((A \in ω \to (A \in z \to G (A) < G (z))) \leftrightarrow (A \in ω \to (A \in y \to G (A) < G (y))))$
13		eleq2	$⊢ z = suc y \to (A \in z \leftrightarrow A \in suc y)$
14		fveq2	$⊢ z = suc y \to G (z) = G (suc y)$
15	14	breq2d	$⊢ z = suc y \to (G (A) < G (z) \leftrightarrow G (A) < G (suc y))$
16	13 15	imbi12d	$⊢ z = suc y \to ((A \in z \to G (A) < G (z)) \leftrightarrow (A \in suc y \to G (A) < G (suc y)))$
17	16	imbi2d	$⊢ z = suc y \to ((A \in ω \to (A \in z \to G (A) < G (z))) \leftrightarrow (A \in ω \to (A \in suc y \to G (A) < G (suc y))))$
18		eleq2	$⊢ z = B \to (A \in z \leftrightarrow A \in B)$
19		fveq2	$⊢ z = B \to G (z) = G (B)$
20	19	breq2d	$⊢ z = B \to (G (A) < G (z) \leftrightarrow G (A) < G (B))$
21	18 20	imbi12d	$⊢ z = B \to ((A \in z \to G (A) < G (z)) \leftrightarrow (A \in B \to G (A) < G (B)))$
22	21	imbi2d	$⊢ z = B \to ((A \in ω \to (A \in z \to G (A) < G (z))) \leftrightarrow (A \in ω \to (A \in B \to G (A) < G (B))))$
23		noel	$⊢ \neg A \in \emptyset$
24	23	pm2.21i	$⊢ A \in \emptyset \to G (A) < G (\emptyset)$
25	24	a1i	$⊢ A \in ω \to (A \in \emptyset \to G (A) < G (\emptyset))$
26		id	$⊢ (A \in y \to G (A) < G (y)) \to (A \in y \to G (A) < G (y))$
27		fveq2	$⊢ A = y \to G (A) = G (y)$
28	27	a1i	$⊢ (A \in y \to G (A) < G (y)) \to (A = y \to G (A) = G (y))$
29	26 28	orim12d	$⊢ (A \in y \to G (A) < G (y)) \to ((A \in y \lor A = y) \to (G (A) < G (y) \lor G (A) = G (y)))$
30		elsuc2g	$⊢ y \in ω \to (A \in suc y \leftrightarrow (A \in y \lor A = y))$
31	30	bicomd	$⊢ y \in ω \to ((A \in y \lor A = y) \leftrightarrow A \in suc y)$
32	31	adantl	$⊢ (A \in ω \land y \in ω) \to ((A \in y \lor A = y) \leftrightarrow A \in suc y)$
33	1 2	om2uzsuci	$⊢ y \in ω \to G (suc y) = G (y) + 1$
34	33	breq2d	$⊢ y \in ω \to (G (A) < G (suc y) \leftrightarrow G (A) < G (y) + 1)$
35	34	adantl	$⊢ (A \in ω \land y \in ω) \to (G (A) < G (suc y) \leftrightarrow G (A) < G (y) + 1)$
36	1 2	om2uzuzi	$⊢ A \in ω \to G (A) \in ℤ_{\geq C}$
37	1 2	om2uzuzi	$⊢ y \in ω \to G (y) \in ℤ_{\geq C}$
38		eluzelz	$⊢ G (A) \in ℤ_{\geq C} \to G (A) \in ℤ$
39		eluzelz	$⊢ G (y) \in ℤ_{\geq C} \to G (y) \in ℤ$
40		zleltp1	$⊢ (G (A) \in ℤ \land G (y) \in ℤ) \to (G (A) \leq G (y) \leftrightarrow G (A) < G (y) + 1)$
41	38 39 40	syl2an	$⊢ (G (A) \in ℤ_{\geq C} \land G (y) \in ℤ_{\geq C}) \to (G (A) \leq G (y) \leftrightarrow G (A) < G (y) + 1)$
42	36 37 41	syl2an	$⊢ (A \in ω \land y \in ω) \to (G (A) \leq G (y) \leftrightarrow G (A) < G (y) + 1)$
43	36 38	syl	$⊢ A \in ω \to G (A) \in ℤ$
44	43	zred	$⊢ A \in ω \to G (A) \in ℝ$
45	37 39	syl	$⊢ y \in ω \to G (y) \in ℤ$
46	45	zred	$⊢ y \in ω \to G (y) \in ℝ$
47		leloe	$⊢ (G (A) \in ℝ \land G (y) \in ℝ) \to (G (A) \leq G (y) \leftrightarrow (G (A) < G (y) \lor G (A) = G (y)))$
48	44 46 47	syl2an	$⊢ (A \in ω \land y \in ω) \to (G (A) \leq G (y) \leftrightarrow (G (A) < G (y) \lor G (A) = G (y)))$
49	35 42 48	3bitr2rd	$⊢ (A \in ω \land y \in ω) \to ((G (A) < G (y) \lor G (A) = G (y)) \leftrightarrow G (A) < G (suc y))$
50	32 49	imbi12d	$⊢ (A \in ω \land y \in ω) \to (((A \in y \lor A = y) \to (G (A) < G (y) \lor G (A) = G (y))) \leftrightarrow (A \in suc y \to G (A) < G (suc y)))$
51	29 50	imbitrid	$⊢ (A \in ω \land y \in ω) \to ((A \in y \to G (A) < G (y)) \to (A \in suc y \to G (A) < G (suc y)))$
52	51	expcom	$⊢ y \in ω \to (A \in ω \to ((A \in y \to G (A) < G (y)) \to (A \in suc y \to G (A) < G (suc y))))$
53	52	a2d	$⊢ y \in ω \to ((A \in ω \to (A \in y \to G (A) < G (y))) \to (A \in ω \to (A \in suc y \to G (A) < G (suc y))))$
54	7 12 17 22 25 53	finds	$⊢ B \in ω \to (A \in ω \to (A \in B \to G (A) < G (B)))$
55	54	impcom	$⊢ (A \in ω \land B \in ω) \to (A \in B \to G (A) < G (B))$

Metamath Proof Explorer

Theorem om2uzlti

Proof