Theorem 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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oaord	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
2	1	3com12	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
3	2	notbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
4		ontri1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
5	4	3adant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
6		oacl	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 +o 𝐴 ) ∈ On )
7	6	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝐴 ) ∈ On )
8	7	3adant2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝐴 ) ∈ On )
9		oacl	⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 +o 𝐵 ) ∈ On )
10	9	ancoms	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝐵 ) ∈ On )
11	10	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝐵 ) ∈ On )
12		ontri1	⊢ ( ( ( 𝐶 +o 𝐴 ) ∈ On ∧ ( 𝐶 +o 𝐵 ) ∈ On ) → ( ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ↔ ¬ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
13	8 11 12	syl2anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ↔ ¬ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
14	3 5 13	3bitr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )