MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oewordri Structured version   Visualization version   GIF version

Theorem oewordri 7956
Description: Weak ordering property of ordinal exponentiation. Proposition 8.35 of [TakeutiZaring] p. 68. (Contributed by NM, 6-Jan-2005.)
Assertion
Ref Expression
oewordri ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝐵 → (𝐴o 𝐶) ⊆ (𝐵o 𝐶)))

Proof of Theorem oewordri
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6930 . . . . 5 (𝑥 = ∅ → (𝐴o 𝑥) = (𝐴o ∅))
2 oveq2 6930 . . . . 5 (𝑥 = ∅ → (𝐵o 𝑥) = (𝐵o ∅))
31, 2sseq12d 3852 . . . 4 (𝑥 = ∅ → ((𝐴o 𝑥) ⊆ (𝐵o 𝑥) ↔ (𝐴o ∅) ⊆ (𝐵o ∅)))
4 oveq2 6930 . . . . 5 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
5 oveq2 6930 . . . . 5 (𝑥 = 𝑦 → (𝐵o 𝑥) = (𝐵o 𝑦))
64, 5sseq12d 3852 . . . 4 (𝑥 = 𝑦 → ((𝐴o 𝑥) ⊆ (𝐵o 𝑥) ↔ (𝐴o 𝑦) ⊆ (𝐵o 𝑦)))
7 oveq2 6930 . . . . 5 (𝑥 = suc 𝑦 → (𝐴o 𝑥) = (𝐴o suc 𝑦))
8 oveq2 6930 . . . . 5 (𝑥 = suc 𝑦 → (𝐵o 𝑥) = (𝐵o suc 𝑦))
97, 8sseq12d 3852 . . . 4 (𝑥 = suc 𝑦 → ((𝐴o 𝑥) ⊆ (𝐵o 𝑥) ↔ (𝐴o suc 𝑦) ⊆ (𝐵o suc 𝑦)))
10 oveq2 6930 . . . . 5 (𝑥 = 𝐶 → (𝐴o 𝑥) = (𝐴o 𝐶))
11 oveq2 6930 . . . . 5 (𝑥 = 𝐶 → (𝐵o 𝑥) = (𝐵o 𝐶))
1210, 11sseq12d 3852 . . . 4 (𝑥 = 𝐶 → ((𝐴o 𝑥) ⊆ (𝐵o 𝑥) ↔ (𝐴o 𝐶) ⊆ (𝐵o 𝐶)))
13 onelon 6001 . . . . . . 7 ((𝐵 ∈ On ∧ 𝐴𝐵) → 𝐴 ∈ On)
14 oe0 7886 . . . . . . 7 (𝐴 ∈ On → (𝐴o ∅) = 1o)
1513, 14syl 17 . . . . . 6 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐴o ∅) = 1o)
16 oe0 7886 . . . . . . 7 (𝐵 ∈ On → (𝐵o ∅) = 1o)
1716adantr 474 . . . . . 6 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐵o ∅) = 1o)
1815, 17eqtr4d 2816 . . . . 5 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐴o ∅) = (𝐵o ∅))
19 eqimss 3875 . . . . 5 ((𝐴o ∅) = (𝐵o ∅) → (𝐴o ∅) ⊆ (𝐵o ∅))
2018, 19syl 17 . . . 4 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐴o ∅) ⊆ (𝐵o ∅))
21 simpl 476 . . . . . 6 ((𝐵 ∈ On ∧ 𝐴𝐵) → 𝐵 ∈ On)
22 onelss 6018 . . . . . . 7 (𝐵 ∈ On → (𝐴𝐵𝐴𝐵))
2322imp 397 . . . . . 6 ((𝐵 ∈ On ∧ 𝐴𝐵) → 𝐴𝐵)
2413, 21, 23jca31 510 . . . . 5 ((𝐵 ∈ On ∧ 𝐴𝐵) → ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴𝐵))
25 oecl 7901 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴o 𝑦) ∈ On)
26253adant2 1122 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴o 𝑦) ∈ On)
27 oecl 7901 . . . . . . . . . . . . . 14 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵o 𝑦) ∈ On)
28273adant1 1121 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵o 𝑦) ∈ On)
29 simp1 1127 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → 𝐴 ∈ On)
30 omwordri 7936 . . . . . . . . . . . . 13 (((𝐴o 𝑦) ∈ On ∧ (𝐵o 𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴o 𝑦) ⊆ (𝐵o 𝑦) → ((𝐴o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐴)))
3126, 28, 29, 30syl3anc 1439 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴o 𝑦) ⊆ (𝐵o 𝑦) → ((𝐴o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐴)))
3231imp 397 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦)) → ((𝐴o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐴))
3332adantrl 706 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴𝐵 ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦))) → ((𝐴o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐴))
34 omwordi 7935 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐵o 𝑦) ∈ On) → (𝐴𝐵 → ((𝐵o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐵)))
3528, 34syld3an3 1477 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴𝐵 → ((𝐵o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐵)))
3635imp 397 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴𝐵) → ((𝐵o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐵))
3736adantrr 707 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴𝐵 ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦))) → ((𝐵o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐵))
3833, 37sstrd 3830 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴𝐵 ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦))) → ((𝐴o 𝑦) ·o 𝐴) ⊆ ((𝐵o 𝑦) ·o 𝐵))
39 oesuc 7891 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴o suc 𝑦) = ((𝐴o 𝑦) ·o 𝐴))
40393adant2 1122 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴o suc 𝑦) = ((𝐴o 𝑦) ·o 𝐴))
4140adantr 474 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴𝐵 ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦))) → (𝐴o suc 𝑦) = ((𝐴o 𝑦) ·o 𝐴))
42 oesuc 7891 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵o suc 𝑦) = ((𝐵o 𝑦) ·o 𝐵))
43423adant1 1121 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵o suc 𝑦) = ((𝐵o 𝑦) ·o 𝐵))
4443adantr 474 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴𝐵 ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦))) → (𝐵o suc 𝑦) = ((𝐵o 𝑦) ·o 𝐵))
4538, 41, 443sstr4d 3866 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴𝐵 ∧ (𝐴o 𝑦) ⊆ (𝐵o 𝑦))) → (𝐴o suc 𝑦) ⊆ (𝐵o suc 𝑦))
4645exp520 1419 . . . . . . 7 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴𝐵 → ((𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o suc 𝑦) ⊆ (𝐵o suc 𝑦))))))
4746com3r 87 . . . . . 6 (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝐴𝐵 → ((𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o suc 𝑦) ⊆ (𝐵o suc 𝑦))))))
4847imp4c 416 . . . . 5 (𝑦 ∈ On → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴𝐵) → ((𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o suc 𝑦) ⊆ (𝐵o suc 𝑦))))
4924, 48syl5 34 . . . 4 (𝑦 ∈ On → ((𝐵 ∈ On ∧ 𝐴𝐵) → ((𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o suc 𝑦) ⊆ (𝐵o suc 𝑦))))
50 vex 3400 . . . . . . . . . . . 12 𝑥 ∈ V
51 limelon 6039 . . . . . . . . . . . 12 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
5250, 51mpan 680 . . . . . . . . . . 11 (Lim 𝑥𝑥 ∈ On)
53 0ellim 6038 . . . . . . . . . . 11 (Lim 𝑥 → ∅ ∈ 𝑥)
54 oe0m1 7885 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ (∅ ↑o 𝑥) = ∅))
5554biimpa 470 . . . . . . . . . . 11 ((𝑥 ∈ On ∧ ∅ ∈ 𝑥) → (∅ ↑o 𝑥) = ∅)
5652, 53, 55syl2anc 579 . . . . . . . . . 10 (Lim 𝑥 → (∅ ↑o 𝑥) = ∅)
57 0ss 4197 . . . . . . . . . 10 ∅ ⊆ (𝐵o 𝑥)
5856, 57syl6eqss 3873 . . . . . . . . 9 (Lim 𝑥 → (∅ ↑o 𝑥) ⊆ (𝐵o 𝑥))
59 oveq1 6929 . . . . . . . . . 10 (𝐴 = ∅ → (𝐴o 𝑥) = (∅ ↑o 𝑥))
6059sseq1d 3850 . . . . . . . . 9 (𝐴 = ∅ → ((𝐴o 𝑥) ⊆ (𝐵o 𝑥) ↔ (∅ ↑o 𝑥) ⊆ (𝐵o 𝑥)))
6158, 60syl5ibr 238 . . . . . . . 8 (𝐴 = ∅ → (Lim 𝑥 → (𝐴o 𝑥) ⊆ (𝐵o 𝑥)))
6261adantl 475 . . . . . . 7 (((𝐵 ∈ On ∧ 𝐴𝐵) ∧ 𝐴 = ∅) → (Lim 𝑥 → (𝐴o 𝑥) ⊆ (𝐵o 𝑥)))
6362a1dd 50 . . . . . 6 (((𝐵 ∈ On ∧ 𝐴𝐵) ∧ 𝐴 = ∅) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o 𝑥) ⊆ (𝐵o 𝑥))))
64 ss2iun 4769 . . . . . . . 8 (∀𝑦𝑥 (𝐴o 𝑦) ⊆ (𝐵o 𝑦) → 𝑦𝑥 (𝐴o 𝑦) ⊆ 𝑦𝑥 (𝐵o 𝑦))
65 oelim 7898 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
6650, 65mpanlr1 696 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
6766an32s 642 . . . . . . . . . 10 (((𝐴 ∈ On ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
6867adantllr 709 . . . . . . . . 9 ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
6921anim1i 608 . . . . . . . . . . 11 (((𝐵 ∈ On ∧ 𝐴𝐵) ∧ Lim 𝑥) → (𝐵 ∈ On ∧ Lim 𝑥))
70 ne0i 4148 . . . . . . . . . . . . . 14 (𝐴𝐵𝐵 ≠ ∅)
71 on0eln0 6031 . . . . . . . . . . . . . 14 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
7270, 71syl5ibr 238 . . . . . . . . . . . . 13 (𝐵 ∈ On → (𝐴𝐵 → ∅ ∈ 𝐵))
7372imp 397 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝐴𝐵) → ∅ ∈ 𝐵)
7473adantr 474 . . . . . . . . . . 11 (((𝐵 ∈ On ∧ 𝐴𝐵) ∧ Lim 𝑥) → ∅ ∈ 𝐵)
75 oelim 7898 . . . . . . . . . . . 12 (((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐵) → (𝐵o 𝑥) = 𝑦𝑥 (𝐵o 𝑦))
7650, 75mpanlr1 696 . . . . . . . . . . 11 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → (𝐵o 𝑥) = 𝑦𝑥 (𝐵o 𝑦))
7769, 74, 76syl2anc 579 . . . . . . . . . 10 (((𝐵 ∈ On ∧ 𝐴𝐵) ∧ Lim 𝑥) → (𝐵o 𝑥) = 𝑦𝑥 (𝐵o 𝑦))
7877ad4ant24 744 . . . . . . . . 9 ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (𝐵o 𝑥) = 𝑦𝑥 (𝐵o 𝑦))
7968, 78sseq12d 3852 . . . . . . . 8 ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → ((𝐴o 𝑥) ⊆ (𝐵o 𝑥) ↔ 𝑦𝑥 (𝐴o 𝑦) ⊆ 𝑦𝑥 (𝐵o 𝑦)))
8064, 79syl5ibr 238 . . . . . . 7 ((((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝑥) → (∀𝑦𝑥 (𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o 𝑥) ⊆ (𝐵o 𝑥)))
8180ex 403 . . . . . 6 (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)) ∧ ∅ ∈ 𝐴) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o 𝑥) ⊆ (𝐵o 𝑥))))
8263, 81oe0lem 7877 . . . . 5 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o 𝑥) ⊆ (𝐵o 𝑥))))
8313ancri 545 . . . . 5 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐴𝐵)))
8482, 83syl11 33 . . . 4 (Lim 𝑥 → ((𝐵 ∈ On ∧ 𝐴𝐵) → (∀𝑦𝑥 (𝐴o 𝑦) ⊆ (𝐵o 𝑦) → (𝐴o 𝑥) ⊆ (𝐵o 𝑥))))
853, 6, 9, 12, 20, 49, 84tfinds3 7342 . . 3 (𝐶 ∈ On → ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐴o 𝐶) ⊆ (𝐵o 𝐶)))
8685expd 406 . 2 (𝐶 ∈ On → (𝐵 ∈ On → (𝐴𝐵 → (𝐴o 𝐶) ⊆ (𝐵o 𝐶))))
8786impcom 398 1 ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝐵 → (𝐴o 𝐶) ⊆ (𝐵o 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071   = wceq 1601  wcel 2106  wne 2968  wral 3089  Vcvv 3397  wss 3791  c0 4140   ciun 4753  Oncon0 5976  Lim wlim 5977  suc csuc 5978  (class class class)co 6922  1oc1o 7836   ·o comu 7841  o coe 7842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-omul 7848  df-oexp 7849
This theorem is referenced by:  oeordsuc  7958
  Copyright terms: Public domain W3C validator