Theorem nnmword

Description: Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	nnmword	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iba	⊢ ( ∅ ∈ 𝐶 → ( 𝐵 ∈ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∧ ∅ ∈ 𝐶 ) ) )
2		nnmord	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐵 ∈ 𝐴 ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
3	2	3com12	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐵 ∈ 𝐴 ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
4	1 3	sylan9bbr	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐵 ∈ 𝐴 ↔ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
5	4	notbid	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
6		simpl1	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → 𝐴 ∈ ω )
7		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
8	6 7	syl	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → 𝐴 ∈ On )
9		simpl2	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → 𝐵 ∈ ω )
10		nnon	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
11	9 10	syl	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → 𝐵 ∈ On )
12		ontri1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
13	8 11 12	syl2anc	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
14		simpl3	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → 𝐶 ∈ ω )
15		nnmcl	⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐶 ·o 𝐴 ) ∈ ω )
16	14 6 15	syl2anc	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ ω )
17		nnon	⊢ ( ( 𝐶 ·o 𝐴 ) ∈ ω → ( 𝐶 ·o 𝐴 ) ∈ On )
18	16 17	syl	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ On )
19		nnmcl	⊢ ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 ·o 𝐵 ) ∈ ω )
20	14 9 19	syl2anc	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐵 ) ∈ ω )
21		nnon	⊢ ( ( 𝐶 ·o 𝐵 ) ∈ ω → ( 𝐶 ·o 𝐵 ) ∈ On )
22	20 21	syl	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐵 ) ∈ On )
23		ontri1	⊢ ( ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
24	18 22 23	syl2anc	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ¬ ( 𝐶 ·o 𝐵 ) ∈ ( 𝐶 ·o 𝐴 ) ) )
25	5 13 24	3bitr4d	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )