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