Theorem omcan

Description: Left cancellation law for ordinal multiplication. Proposition 8.20 of TakeutiZaring p. 63 and its converse. (Contributed by NM, 14-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		omordi	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
2	1	ex	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) ) )
3	2	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) ) )
5	4	imp	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
6		omordi	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
7	6	ex	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
8	7	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
9	8	3adant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
10	9	imp	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
11	5 10	orim12d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
12	11	con3d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) → ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
13		omcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
14		eloni	⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → Ord ( 𝐴 ·o 𝐵 ) )
15	13 14	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord ( 𝐴 ·o 𝐵 ) )
16		omcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ·o 𝐶 ) ∈ On )
17		eloni	⊢ ( ( 𝐴 ·o 𝐶 ) ∈ On → Ord ( 𝐴 ·o 𝐶 ) )
18	16 17	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → Ord ( 𝐴 ·o 𝐶 ) )
19		ordtri3	⊢ ( ( Ord ( 𝐴 ·o 𝐵 ) ∧ Ord ( 𝐴 ·o 𝐶 ) ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
20	15 18 19	syl2an	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
21	20	3impdi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
22	21	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
23		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
24		eloni	⊢ ( 𝐶 ∈ On → Ord 𝐶 )
25		ordtri3	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
26	23 24 25	syl2an	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
27	26	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
28	27	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
29	12 22 28	3imtr4d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) → 𝐵 = 𝐶 ) )
30		oveq2	⊢ ( 𝐵 = 𝐶 → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) )
31	29 30	impbid1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ 𝐵 = 𝐶 ) )