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