nnawordi

Description: Adding to both sides of an inequality in _om . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 12-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to A +_{𝑜} x = A +_{𝑜} \emptyset$
2		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
3	1 2	sseq12d	$⊢ x = \emptyset \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset)$
4	3	imbi2d	$⊢ x = \emptyset \to ((A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x) \leftrightarrow (A \subseteq B \to A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset))$
5	4	imbi2d	$⊢ x = \emptyset \to (((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x)) \leftrightarrow ((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset)))$
6		oveq2	$⊢ x = y \to A +_{𝑜} x = A +_{𝑜} y$
7		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
8	6 7	sseq12d	$⊢ x = y \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} y \subseteq B +_{𝑜} y)$
9	8	imbi2d	$⊢ x = y \to ((A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x) \leftrightarrow (A \subseteq B \to A +_{𝑜} y \subseteq B +_{𝑜} y))$
10	9	imbi2d	$⊢ x = y \to (((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x)) \leftrightarrow ((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} y \subseteq B +_{𝑜} y)))$
11		oveq2	$⊢ x = suc y \to A +_{𝑜} x = A +_{𝑜} suc y$
12		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
13	11 12	sseq12d	$⊢ x = suc y \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)$
14	13	imbi2d	$⊢ x = suc y \to ((A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x) \leftrightarrow (A \subseteq B \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y))$
15	14	imbi2d	$⊢ x = suc y \to (((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x)) \leftrightarrow ((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)))$
16		oveq2	$⊢ x = C \to A +_{𝑜} x = A +_{𝑜} C$
17		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
18	16 17	sseq12d	$⊢ x = C \to (A +_{𝑜} x \subseteq B +_{𝑜} x \leftrightarrow A +_{𝑜} C \subseteq B +_{𝑜} C)$
19	18	imbi2d	$⊢ x = C \to ((A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x) \leftrightarrow (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C))$
20	19	imbi2d	$⊢ x = C \to (((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} x \subseteq B +_{𝑜} x)) \leftrightarrow ((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C)))$
21		nnon	$⊢ A \in ω \to A \in On$
22		nnon	$⊢ B \in ω \to B \in On$
23		oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$
24	23	adantr	$⊢ (A \in On \land B \in On) \to A +_{𝑜} \emptyset = A$
25		oa0	$⊢ B \in On \to B +_{𝑜} \emptyset = B$
26	25	adantl	$⊢ (A \in On \land B \in On) \to B +_{𝑜} \emptyset = B$
27	24 26	sseq12d	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset \leftrightarrow A \subseteq B)$
28	27	biimprd	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset)$
29	21 22 28	syl2an	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} \emptyset \subseteq B +_{𝑜} \emptyset)$
30		nnacl	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} y \in ω$
31	30	ancoms	$⊢ (y \in ω \land A \in ω) \to A +_{𝑜} y \in ω$
32	31	adantrr	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to A +_{𝑜} y \in ω$
33		nnon	$⊢ A +_{𝑜} y \in ω \to A +_{𝑜} y \in On$
34		eloni	$⊢ A +_{𝑜} y \in On \to Ord (A +_{𝑜} y)$
35	32 33 34	3syl	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to Ord (A +_{𝑜} y)$
36		nnacl	$⊢ (B \in ω \land y \in ω) \to B +_{𝑜} y \in ω$
37	36	ancoms	$⊢ (y \in ω \land B \in ω) \to B +_{𝑜} y \in ω$
38	37	adantrl	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to B +_{𝑜} y \in ω$
39		nnon	$⊢ B +_{𝑜} y \in ω \to B +_{𝑜} y \in On$
40		eloni	$⊢ B +_{𝑜} y \in On \to Ord (B +_{𝑜} y)$
41	38 39 40	3syl	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to Ord (B +_{𝑜} y)$
42		ordsucsssuc	$⊢ (Ord (A +_{𝑜} y) \land Ord (B +_{𝑜} y)) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
43	35 41 42	syl2anc	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
44	43	biimpa	$⊢ ((y \in ω \land (A \in ω \land B \in ω)) \land A +_{𝑜} y \subseteq B +_{𝑜} y) \to suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y)$
45		nnasuc	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
46	45	ancoms	$⊢ (y \in ω \land A \in ω) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
47	46	adantrr	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
48		nnasuc	$⊢ (B \in ω \land y \in ω) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
49	48	ancoms	$⊢ (y \in ω \land B \in ω) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
50	49	adantrl	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
51	47 50	sseq12d	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to (A +_{𝑜} suc y \subseteq B +_{𝑜} suc y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
52	51	adantr	$⊢ ((y \in ω \land (A \in ω \land B \in ω)) \land A +_{𝑜} y \subseteq B +_{𝑜} y) \to (A +_{𝑜} suc y \subseteq B +_{𝑜} suc y \leftrightarrow suc (A +_{𝑜} y) \subseteq suc (B +_{𝑜} y))$
53	44 52	mpbird	$⊢ ((y \in ω \land (A \in ω \land B \in ω)) \land A +_{𝑜} y \subseteq B +_{𝑜} y) \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y$
54	53	ex	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to (A +_{𝑜} y \subseteq B +_{𝑜} y \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)$
55	54	imim2d	$⊢ (y \in ω \land (A \in ω \land B \in ω)) \to ((A \subseteq B \to A +_{𝑜} y \subseteq B +_{𝑜} y) \to (A \subseteq B \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y))$
56	55	ex	$⊢ y \in ω \to ((A \in ω \land B \in ω) \to ((A \subseteq B \to A +_{𝑜} y \subseteq B +_{𝑜} y) \to (A \subseteq B \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)))$
57	56	a2d	$⊢ y \in ω \to (((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} y \subseteq B +_{𝑜} y)) \to ((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} suc y \subseteq B +_{𝑜} suc y)))$
58	5 10 15 20 29 57	finds	$⊢ C \in ω \to ((A \in ω \land B \in ω) \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C))$
59	58	com12	$⊢ (A \in ω \land B \in ω) \to (C \in ω \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C))$
60	59	3impia	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \subseteq B \to A +_{𝑜} C \subseteq B +_{𝑜} C)$

Metamath Proof Explorer

Theorem nnawordi

Proof