oaword

Description: Weak ordering property of ordinal addition. (Contributed by NM, 6-Dec-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Step	Hyp	Ref	Expression
1		oaord	$⊢ (B \in On \land A \in On \land C \in On) \to (B \in A \leftrightarrow C +_{𝑜} B \in (C +_{𝑜} A))$
2	1	3com12	$⊢ (A \in On \land B \in On \land C \in On) \to (B \in A \leftrightarrow C +_{𝑜} B \in (C +_{𝑜} A))$
3	2	notbid	$⊢ (A \in On \land B \in On \land C \in On) \to (\neg B \in A \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
4		ontri1	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow \neg B \in A)$
5	4	3adant3	$⊢ (A \in On \land B \in On \land C \in On) \to (A \subseteq B \leftrightarrow \neg B \in A)$
6		oacl	$⊢ (C \in On \land A \in On) \to C +_{𝑜} A \in On$
7	6	ancoms	$⊢ (A \in On \land C \in On) \to C +_{𝑜} A \in On$
8	7	3adant2	$⊢ (A \in On \land B \in On \land C \in On) \to C +_{𝑜} A \in On$
9		oacl	$⊢ (C \in On \land B \in On) \to C +_{𝑜} B \in On$
10	9	ancoms	$⊢ (B \in On \land C \in On) \to C +_{𝑜} B \in On$
11	10	3adant1	$⊢ (A \in On \land B \in On \land C \in On) \to C +_{𝑜} B \in On$
12		ontri1	$⊢ (C +_{𝑜} A \in On \land C +_{𝑜} B \in On) \to (C +_{𝑜} A \subseteq C +_{𝑜} B \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
13	8 11 12	syl2anc	$⊢ (A \in On \land B \in On \land C \in On) \to (C +_{𝑜} A \subseteq C +_{𝑜} B \leftrightarrow \neg C +_{𝑜} B \in (C +_{𝑜} A))$
14	3 5 13	3bitr4d	$⊢ (A \in On \land B \in On \land C \in On) \to (A \subseteq B \leftrightarrow C +_{𝑜} A \subseteq C +_{𝑜} B)$

Metamath Proof Explorer