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