Metamath Proof Explorer

Theorem omwordri

Description: Weak ordering property of ordinal multiplication. Proposition 8.21 of TakeutiZaring p. 63. (Contributed by NM, 20-Dec-2004)

Ref Expression
Assertion omwordri ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ·o 𝐶 ) ⊆ ( 𝐵 ·o 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o ∅ ) )
2 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o ∅ ) )
3 1 2 sseq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ↔ ( 𝐴 ·o ∅ ) ⊆ ( 𝐵 ·o ∅ ) ) )
4 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑦 ) )
5 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o 𝑦 ) )
6 4 5 sseq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ↔ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) )
7 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o suc 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o suc 𝑦 ) )
9 7 8 sseq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ↔ ( 𝐴 ·o suc 𝑦 ) ⊆ ( 𝐵 ·o suc 𝑦 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐶 ) )
11 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o 𝐶 ) )
12 10 11 sseq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ↔ ( 𝐴 ·o 𝐶 ) ⊆ ( 𝐵 ·o 𝐶 ) ) )
13 om0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
14 0ss ⊢ ∅ ⊆ ( 𝐵 ·o ∅ )
15 13 14 eqsstrdi ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) ⊆ ( 𝐵 ·o ∅ ) )
16 15 ad2antrr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ·o ∅ ) ⊆ ( 𝐵 ·o ∅ ) )
17 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o 𝑦 ) ∈ On )
18 17 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o 𝑦 ) ∈ On )
19 omcl ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ·o 𝑦 ) ∈ On )
20 19 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ·o 𝑦 ) ∈ On )
21 simp1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → 𝐴 ∈ On )
22 oawordri ⊢ ( ( ( 𝐴 ·o 𝑦 ) ∈ On ∧ ( 𝐵 ·o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) ) )
23 18 20 21 22 syl3anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) ) )
24 23 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) )
25 24 adantrl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) )
26 oaword ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ( 𝐵 ·o 𝑦 ) ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) )
27 20 26 syld3an3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) )
28 27 biimpa ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
29 28 adantrr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) ) → ( ( 𝐵 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
30 25 29 sstrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ⊆ ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
31 omsuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
32 31 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
34 omsuc ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ·o suc 𝑦 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
35 34 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ·o suc 𝑦 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) ) → ( 𝐵 ·o suc 𝑦 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
37 30 33 36 3sstr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) ) ) → ( 𝐴 ·o suc 𝑦 ) ⊆ ( 𝐵 ·o suc 𝑦 ) )
38 37 exp520 ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑦 ∈ On → ( 𝐴 ⊆ 𝐵 → ( ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o suc 𝑦 ) ⊆ ( 𝐵 ·o suc 𝑦 ) ) ) ) ) )
39 38 com3r ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ⊆ 𝐵 → ( ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o suc 𝑦 ) ⊆ ( 𝐵 ·o suc 𝑦 ) ) ) ) ) )
40 39 imp4c ⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o suc 𝑦 ) ⊆ ( 𝐵 ·o suc 𝑦 ) ) ) )
41 vex ⊢ 𝑥 ∈ V
42 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ∪ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) )
43 omlim ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐴 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) )
44 43 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ) → ( 𝐴 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) )
45 omlim ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐵 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) )
46 45 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ) → ( 𝐵 ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) )
47 44 46 sseq12d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ) → ( ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ↔ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐵 ·o 𝑦 ) ) )
48 42 47 syl5ibr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ) )
49 48 anandirs ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ) )
50 41 49 mpanr1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ) )
51 50 expcom ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ) ) )
52 51 adantrd ⊢ ( Lim 𝑥 → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o 𝑦 ) ⊆ ( 𝐵 ·o 𝑦 ) → ( 𝐴 ·o 𝑥 ) ⊆ ( 𝐵 ·o 𝑥 ) ) ) )
53 3 6 9 12 16 40 52 tfinds3 ⊢ ( 𝐶 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ·o 𝐶 ) ⊆ ( 𝐵 ·o 𝐶 ) ) )
54 53 expd ⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ·o 𝐶 ) ⊆ ( 𝐵 ·o 𝐶 ) ) ) )
55 54 3impib ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ·o 𝐶 ) ⊆ ( 𝐵 ·o 𝐶 ) ) )
56 55 3coml ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ·o 𝐶 ) ⊆ ( 𝐵 ·o 𝐶 ) ) )