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

Metamath Proof Explorer

Theorem omword

Description: Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 omord2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
2 3anrot ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) ↔ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) )
3 omcan ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ↔ 𝐴 = 𝐵 ) )
4 2 3 sylanbr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ↔ 𝐴 = 𝐵 ) )
5 4 bicomd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 = 𝐵 ↔ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) )
6 1 5 orbi12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) )
7 onsseleq ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
8 7 3adant3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
10 omcl ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ·o 𝐴 ) ∈ On )
11 omcl ⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ·o 𝐵 ) ∈ On )
12 10 11 anim12dan ⊢ ( ( 𝐶 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) )
13 12 ancoms ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) )
14 13 3impa ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) )
15 onsseleq ⊢ ( ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) )
16 14 15 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) )
17 16 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) )
18 6 9 17 3bitr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )