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

Metamath Proof Explorer

Theorem omord

Description: Ordering property of ordinal multiplication. Proposition 8.19 of TakeutiZaring p. 63. Theorem 3.16 of Schloeder p. 9. (Contributed by NM, 14-Dec-2004)

Ref Expression
Assertion omord ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 omord2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
2 1 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
3 2 pm5.32rd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∧ ∅ ∈ 𝐶 ) ) )
4 simpl ⊢ ( ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) )
5 ne0i ⊢ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → ( 𝐶 ·o 𝐵 ) ≠ ∅ )
6 om0r ⊢ ( 𝐵 ∈ On → ( ∅ ·o 𝐵 ) = ∅ )
7 oveq1 ⊢ ( 𝐶 = ∅ → ( 𝐶 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
8 7 eqeq1d ⊢ ( 𝐶 = ∅ → ( ( 𝐶 ·o 𝐵 ) = ∅ ↔ ( ∅ ·o 𝐵 ) = ∅ ) )
9 6 8 syl5ibrcom ⊢ ( 𝐵 ∈ On → ( 𝐶 = ∅ → ( 𝐶 ·o 𝐵 ) = ∅ ) )
10 9 necon3d ⊢ ( 𝐵 ∈ On → ( ( 𝐶 ·o 𝐵 ) ≠ ∅ → 𝐶 ≠ ∅ ) )
11 5 10 syl5 ⊢ ( 𝐵 ∈ On → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → 𝐶 ≠ ∅ ) )
12 11 adantr ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → 𝐶 ≠ ∅ ) )
13 on0eln0 ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅ ) )
14 13 adantl ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅ ) )
15 12 14 sylibrd ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → ∅ ∈ 𝐶 ) )
16 15 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → ∅ ∈ 𝐶 ) )
17 16 ancld ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∧ ∅ ∈ 𝐶 ) ) )
18 4 17 impbid2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
19 3 18 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )