nnaordi

Description: Ordering property of addition. Proposition 8.4 of TakeutiZaring p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996) (Revised by Mario Carneiro, 15-Nov-2014)

		Ref	Expression
	Assertion	nnaordi	$⊢ (B \in ω \land C \in ω) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$

Proof

Step	Hyp	Ref	Expression
1		elnn	$⊢ (A \in B \land B \in ω) \to A \in ω$
2	1	ancoms	$⊢ (B \in ω \land A \in B) \to A \in ω$
3	2	adantll	$⊢ ((C \in ω \land B \in ω) \land A \in B) \to A \in ω$
4		nnord	$⊢ B \in ω \to Ord B$
5		ordsucss	$⊢ Ord B \to (A \in B \to suc A \subseteq B)$
6	4 5	syl	$⊢ B \in ω \to (A \in B \to suc A \subseteq B)$
7	6	ad2antlr	$⊢ ((C \in ω \land B \in ω) \land A \in ω) \to (A \in B \to suc A \subseteq B)$
8		peano2b	$⊢ A \in ω \leftrightarrow suc A \in ω$
9		oveq2	$⊢ x = suc A \to C +_{𝑜} x = C +_{𝑜} suc A$
10	9	sseq2d	$⊢ x = suc A \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} suc A)$
11	10	imbi2d	$⊢ x = suc A \to ((C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc A))$
12		oveq2	$⊢ x = y \to C +_{𝑜} x = C +_{𝑜} y$
13	12	sseq2d	$⊢ x = y \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} y)$
14	13	imbi2d	$⊢ x = y \to ((C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} y))$
15		oveq2	$⊢ x = suc y \to C +_{𝑜} x = C +_{𝑜} suc y$
16	15	sseq2d	$⊢ x = suc y \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} suc y)$
17	16	imbi2d	$⊢ x = suc y \to ((C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
18		oveq2	$⊢ x = B \to C +_{𝑜} x = C +_{𝑜} B$
19	18	sseq2d	$⊢ x = B \to (C +_{𝑜} suc A \subseteq C +_{𝑜} x \leftrightarrow C +_{𝑜} suc A \subseteq C +_{𝑜} B)$
20	19	imbi2d	$⊢ x = B \to ((C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} x) \leftrightarrow (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} B))$
21		ssid	$⊢ C +_{𝑜} suc A \subseteq C +_{𝑜} suc A$
22	21	2a1i	$⊢ suc A \in ω \to (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc A)$
23		sssucid	$⊢ C +_{𝑜} y \subseteq suc (C +_{𝑜} y)$
24		sstr2	$⊢ C +_{𝑜} suc A \subseteq C +_{𝑜} y \to (C +_{𝑜} y \subseteq suc (C +_{𝑜} y) \to C +_{𝑜} suc A \subseteq suc (C +_{𝑜} y))$
25	23 24	mpi	$⊢ C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq suc (C +_{𝑜} y)$
26		nnasuc	$⊢ (C \in ω \land y \in ω) \to C +_{𝑜} suc y = suc (C +_{𝑜} y)$
27	26	ancoms	$⊢ (y \in ω \land C \in ω) \to C +_{𝑜} suc y = suc (C +_{𝑜} y)$
28	27	sseq2d	$⊢ (y \in ω \land C \in ω) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} suc y \leftrightarrow C +_{𝑜} suc A \subseteq suc (C +_{𝑜} y))$
29	25 28	imbitrrid	$⊢ (y \in ω \land C \in ω) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y)$
30	29	ex	$⊢ y \in ω \to (C \in ω \to (C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
31	30	ad2antrr	$⊢ ((y \in ω \land suc A \in ω) \land suc A \subseteq y) \to (C \in ω \to (C +_{𝑜} suc A \subseteq C +_{𝑜} y \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
32	31	a2d	$⊢ ((y \in ω \land suc A \in ω) \land suc A \subseteq y) \to ((C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} y) \to (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} suc y))$
33	11 14 17 20 22 32	findsg	$⊢ ((B \in ω \land suc A \in ω) \land suc A \subseteq B) \to (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)$
34	33	exp31	$⊢ B \in ω \to (suc A \in ω \to (suc A \subseteq B \to (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)))$
35	8 34	biimtrid	$⊢ B \in ω \to (A \in ω \to (suc A \subseteq B \to (C \in ω \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)))$
36	35	com4r	$⊢ C \in ω \to (B \in ω \to (A \in ω \to (suc A \subseteq B \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)))$
37	36	imp31	$⊢ ((C \in ω \land B \in ω) \land A \in ω) \to (suc A \subseteq B \to C +_{𝑜} suc A \subseteq C +_{𝑜} B)$
38		nnasuc	$⊢ (C \in ω \land A \in ω) \to C +_{𝑜} suc A = suc (C +_{𝑜} A)$
39	38	sseq1d	$⊢ (C \in ω \land A \in ω) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} B \leftrightarrow suc (C +_{𝑜} A) \subseteq C +_{𝑜} B)$
40		ovex	$⊢ C +_{𝑜} A \in V$
41		sucssel	$⊢ C +_{𝑜} A \in V \to (suc (C +_{𝑜} A) \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B))$
42	40 41	ax-mp	$⊢ suc (C +_{𝑜} A) \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B)$
43	39 42	biimtrdi	$⊢ (C \in ω \land A \in ω) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B))$
44	43	adantlr	$⊢ ((C \in ω \land B \in ω) \land A \in ω) \to (C +_{𝑜} suc A \subseteq C +_{𝑜} B \to C +_{𝑜} A \in (C +_{𝑜} B))$
45	7 37 44	3syld	$⊢ ((C \in ω \land B \in ω) \land A \in ω) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$
46	45	imp	$⊢ (((C \in ω \land B \in ω) \land A \in ω) \land A \in B) \to C +_{𝑜} A \in (C +_{𝑜} B)$
47	46	an32s	$⊢ (((C \in ω \land B \in ω) \land A \in B) \land A \in ω) \to C +_{𝑜} A \in (C +_{𝑜} B)$
48	3 47	mpdan	$⊢ ((C \in ω \land B \in ω) \land A \in B) \to C +_{𝑜} A \in (C +_{𝑜} B)$
49	48	ex	$⊢ (C \in ω \land B \in ω) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$
50	49	ancoms	$⊢ (B \in ω \land C \in ω) \to (A \in B \to C +_{𝑜} A \in (C +_{𝑜} B))$

Metamath Proof Explorer

Theorem nnaordi

Proof