Metamath Proof Explorer

Theorem omord2

Description: Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 omordi ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
2 1 3adantl1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
3 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) )
4 3 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 = 𝐵 → ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) )
5 omordi ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐵 ∈ 𝐴 → ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
6 5 3adantl2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐵 ∈ 𝐴 → ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
7 4 6 orim12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) → ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
8 7 con3d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) → ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
9 omcl ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ·o 𝐴 ) ∈ On )
10 omcl ⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ·o 𝐵 ) ∈ On )
11 eloni ⊢ ( ( 𝐶 ·o 𝐴 ) ∈ On → Ord ( 𝐶 ·o 𝐴 ) )
12 eloni ⊢ ( ( 𝐶 ·o 𝐵 ) ∈ On → Ord ( 𝐶 ·o 𝐵 ) )
13 ordtri2 ⊢ ( ( Ord ( 𝐶 ·o 𝐴 ) ∧ Ord ( 𝐶 ·o 𝐵 ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
14 11 12 13 syl2an ⊢ ( ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
15 9 10 14 syl2an ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
16 15 anandis ⊢ ( ( 𝐶 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
17 16 ancoms ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
18 17 3impa ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) ) )
20 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
21 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
22 ordtri2 ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
23 20 21 22 syl2an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
24 23 3adant3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
25 24 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
26 8 19 25 3imtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) → 𝐴 ∈ 𝐵 ) )
27 2 26 impbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )