nnaword

Description: Weak ordering property of addition. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nnaord	$⊢ (B \in ω \land A \in ω \land C \in ω) \to (B \in A \leftrightarrow C +_{𝑜} B \in (C +_{𝑜} A))$
2	1	3com12	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (B \in A \leftrightarrow C +_{𝑜} B \in (C +_{𝑜} A))$
3	2	notbid	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (\neg B \in A \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
4		nnord	$⊢ A \in ω \to Ord A$
5		nnord	$⊢ B \in ω \to Ord B$
6		ordtri1	$⊢ (Ord A \land Ord B) \to (A \subseteq B \leftrightarrow \neg B \in A)$
7	4 5 6	syl2an	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \leftrightarrow \neg B \in A)$
8	7	3adant3	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \subseteq B \leftrightarrow \neg B \in A)$
9		nnacl	$⊢ (C \in ω \land A \in ω) \to C +_{𝑜} A \in ω$
10	9	ancoms	$⊢ (A \in ω \land C \in ω) \to C +_{𝑜} A \in ω$
11	10	3adant2	$⊢ (A \in ω \land B \in ω \land C \in ω) \to C +_{𝑜} A \in ω$
12		nnacl	$⊢ (C \in ω \land B \in ω) \to C +_{𝑜} B \in ω$
13	12	ancoms	$⊢ (B \in ω \land C \in ω) \to C +_{𝑜} B \in ω$
14	13	3adant1	$⊢ (A \in ω \land B \in ω \land C \in ω) \to C +_{𝑜} B \in ω$
15		nnord	$⊢ C +_{𝑜} A \in ω \to Ord (C +_{𝑜} A)$
16		nnord	$⊢ C +_{𝑜} B \in ω \to Ord (C +_{𝑜} B)$
17		ordtri1	$⊢ (Ord (C +_{𝑜} A) \land Ord (C +_{𝑜} B)) \to (C +_{𝑜} A \subseteq C +_{𝑜} B \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
18	15 16 17	syl2an	$⊢ (C +_{𝑜} A \in ω \land C +_{𝑜} B \in ω) \to (C +_{𝑜} A \subseteq C +_{𝑜} B \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
19	11 14 18	syl2anc	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (C +_{𝑜} A \subseteq C +_{𝑜} B \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
20	3 8 19	3bitr4d	$⊢ (A \in ω \land B \in ω \land C \in ω) \to (A \subseteq B \leftrightarrow C +_{𝑜} A \subseteq C +_{𝑜} B)$

Metamath Proof Explorer

Theorem nnaword

Proof