This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) ) )