Metamath Proof Explorer

Theorem oaordi

Description: Ordering property of ordinal addition. Proposition 8.4 of TakeutiZaring p. 58. (Contributed by NM, 5-Dec-2004)

Ref Expression
Assertion oaordi ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
2 1 adantll ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
3 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
4 ordsucss ⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
5 3 4 syl ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
6 5 ad2antlr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
7 sucelon ⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )
8 oveq2 ⊢ ( 𝑥 = suc 𝐴 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o suc 𝐴 ) )
9 8 sseq2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) )
10 9 imbi2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) ) )
11 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o 𝑦 ) )
12 11 sseq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) ) )
14 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o suc 𝑦 ) )
15 14 sseq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) )
16 15 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
17 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o 𝐵 ) )
18 17 sseq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
19 18 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) )
20 ssid ⊢ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 )
21 20 2a1i ⊢ ( suc 𝐴 ∈ On → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) )
22 sssucid ⊢ ( 𝐶 +o 𝑦 ) ⊆ suc ( 𝐶 +o 𝑦 )
23 sstr2 ⊢ ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( ( 𝐶 +o 𝑦 ) ⊆ suc ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) )
24 22 23 mpi ⊢ ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) )
25 oasuc ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 +o suc 𝑦 ) = suc ( 𝐶 +o 𝑦 ) )
26 25 ancoms ⊢ ( ( 𝑦 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 +o suc 𝑦 ) = suc ( 𝐶 +o 𝑦 ) )
27 26 sseq2d ⊢ ( ( 𝑦 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) )
28 24 27 syl5ibr ⊢ ( ( 𝑦 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) )
29 28 ex ⊢ ( 𝑦 ∈ On → ( 𝐶 ∈ On → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
30 29 ad2antrr ⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( 𝐶 ∈ On → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
31 30 a2d ⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
32 sucssel ⊢ ( 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝑥 → 𝐴 ∈ 𝑥 ) )
33 7 32 sylbir ⊢ ( suc 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝑥 → 𝐴 ∈ 𝑥 ) )
34 limsuc ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) )
35 34 biimpd ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → suc 𝐴 ∈ 𝑥 ) )
36 33 35 sylan9r ⊢ ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) → ( suc 𝐴 ⊆ 𝑥 → suc 𝐴 ∈ 𝑥 ) )
37 36 imp ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → suc 𝐴 ∈ 𝑥 )
38 oveq2 ⊢ ( 𝑦 = suc 𝐴 → ( 𝐶 +o 𝑦 ) = ( 𝐶 +o suc 𝐴 ) )
39 38 ssiun2s ⊢ ( suc 𝐴 ∈ 𝑥 → ( 𝐶 +o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
40 37 39 syl ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
41 40 adantr ⊢ ( ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o suc 𝐴 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
42 vex ⊢ 𝑥 ∈ V
43 oalim ⊢ ( ( 𝐶 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
44 42 43 mpanr1 ⊢ ( ( 𝐶 ∈ On ∧ Lim 𝑥 ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
45 44 ancoms ⊢ ( ( Lim 𝑥 ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
46 45 adantlr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
47 46 adantlr ⊢ ( ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐶 +o 𝑦 ) )
48 41 47 sseqtrrd ⊢ ( ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) ∧ 𝐶 ∈ On ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) )
49 48 ex ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) )
50 49 a1d ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐴 ⊆ 𝑦 → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ) )
51 10 13 16 19 21 31 50 tfindsg ⊢ ( ( ( 𝐵 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝐵 ) → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
52 51 exp31 ⊢ ( 𝐵 ∈ On → ( suc 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) )
53 7 52 syl5bi ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ On → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) )
54 53 com4r ⊢ ( 𝐶 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) )
55 54 imp31 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
56 oasuc ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 +o suc 𝐴 ) = suc ( 𝐶 +o 𝐴 ) )
57 56 sseq1d ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ↔ suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
58 ovex ⊢ ( 𝐶 +o 𝐴 ) ∈ V
59 sucssel ⊢ ( ( 𝐶 +o 𝐴 ) ∈ V → ( suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
60 58 59 ax-mp ⊢ ( suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
61 57 60 syl6bi ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
62 61 adantlr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
63 6 55 62 3syld ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
64 63 imp ⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
65 64 an32s ⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) ∧ 𝐴 ∈ On ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
66 2 65 mpdan ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
67 66 ex ⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
68 67 ancoms ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )