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

Theorem oeordi 8200
 Description: Ordering law for ordinal exponentiation. Proposition 8.33 of [TakeutiZaring] p. 67. (Contributed by NM, 5-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
Assertion
Ref Expression
oeordi ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖ 2o)) → (𝐴𝐵 → (𝐶o 𝐴) ∈ (𝐶o 𝐵)))

Proof of Theorem oeordi
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7147 . . . . 5 (𝑥 = suc 𝐴 → (𝐶o 𝑥) = (𝐶o suc 𝐴))
21eleq2d 2878 . . . 4 (𝑥 = suc 𝐴 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
32imbi2d 344 . . 3 (𝑥 = suc 𝐴 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
4 oveq2 7147 . . . . 5 (𝑥 = 𝑦 → (𝐶o 𝑥) = (𝐶o 𝑦))
54eleq2d 2878 . . . 4 (𝑥 = 𝑦 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o 𝑦)))
65imbi2d 344 . . 3 (𝑥 = 𝑦 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
7 oveq2 7147 . . . . 5 (𝑥 = suc 𝑦 → (𝐶o 𝑥) = (𝐶o suc 𝑦))
87eleq2d 2878 . . . 4 (𝑥 = suc 𝑦 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o suc 𝑦)))
98imbi2d 344 . . 3 (𝑥 = suc 𝑦 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦))))
10 oveq2 7147 . . . . 5 (𝑥 = 𝐵 → (𝐶o 𝑥) = (𝐶o 𝐵))
1110eleq2d 2878 . . . 4 (𝑥 = 𝐵 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o 𝐵)))
1211imbi2d 344 . . 3 (𝑥 = 𝐵 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝐵))))
13 eldifi 4057 . . . . . . . 8 (𝐶 ∈ (On ∖ 2o) → 𝐶 ∈ On)
14 oecl 8149 . . . . . . . 8 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ On)
1513, 14sylan 583 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ On)
16 om1 8155 . . . . . . 7 ((𝐶o 𝐴) ∈ On → ((𝐶o 𝐴) ·o 1o) = (𝐶o 𝐴))
1715, 16syl 17 . . . . . 6 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ((𝐶o 𝐴) ·o 1o) = (𝐶o 𝐴))
18 ondif2 8114 . . . . . . . . 9 (𝐶 ∈ (On ∖ 2o) ↔ (𝐶 ∈ On ∧ 1o𝐶))
1918simprbi 500 . . . . . . . 8 (𝐶 ∈ (On ∖ 2o) → 1o𝐶)
2019adantr 484 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 1o𝐶)
2113adantr 484 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐶 ∈ On)
22 simpr 488 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐴 ∈ On)
23 dif20el 8117 . . . . . . . . . 10 (𝐶 ∈ (On ∖ 2o) → ∅ ∈ 𝐶)
2423adantr 484 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ∅ ∈ 𝐶)
25 oen0 8199 . . . . . . . . 9 (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐶) → ∅ ∈ (𝐶o 𝐴))
2621, 22, 24, 25syl21anc 836 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ∅ ∈ (𝐶o 𝐴))
27 omordi 8179 . . . . . . . 8 (((𝐶 ∈ On ∧ (𝐶o 𝐴) ∈ On) ∧ ∅ ∈ (𝐶o 𝐴)) → (1o𝐶 → ((𝐶o 𝐴) ·o 1o) ∈ ((𝐶o 𝐴) ·o 𝐶)))
2821, 15, 26, 27syl21anc 836 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (1o𝐶 → ((𝐶o 𝐴) ·o 1o) ∈ ((𝐶o 𝐴) ·o 𝐶)))
2920, 28mpd 15 . . . . . 6 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ((𝐶o 𝐴) ·o 1o) ∈ ((𝐶o 𝐴) ·o 𝐶))
3017, 29eqeltrrd 2894 . . . . 5 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ ((𝐶o 𝐴) ·o 𝐶))
31 oesuc 8139 . . . . . 6 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶o suc 𝐴) = ((𝐶o 𝐴) ·o 𝐶))
3213, 31sylan 583 . . . . 5 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o suc 𝐴) = ((𝐶o 𝐴) ·o 𝐶))
3330, 32eleqtrrd 2896 . . . 4 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))
3433expcom 417 . . 3 (𝐴 ∈ On → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
35 oecl 8149 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ On)
3613, 35sylan 583 . . . . . . . . . 10 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ On)
37 om1 8155 . . . . . . . . . 10 ((𝐶o 𝑦) ∈ On → ((𝐶o 𝑦) ·o 1o) = (𝐶o 𝑦))
3836, 37syl 17 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ((𝐶o 𝑦) ·o 1o) = (𝐶o 𝑦))
3919adantr 484 . . . . . . . . . 10 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → 1o𝐶)
4013adantr 484 . . . . . . . . . . 11 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → 𝐶 ∈ On)
41 simpr 488 . . . . . . . . . . . 12 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → 𝑦 ∈ On)
4223adantr 484 . . . . . . . . . . . 12 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ∅ ∈ 𝐶)
43 oen0 8199 . . . . . . . . . . . 12 (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ 𝐶) → ∅ ∈ (𝐶o 𝑦))
4440, 41, 42, 43syl21anc 836 . . . . . . . . . . 11 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ∅ ∈ (𝐶o 𝑦))
45 omordi 8179 . . . . . . . . . . 11 (((𝐶 ∈ On ∧ (𝐶o 𝑦) ∈ On) ∧ ∅ ∈ (𝐶o 𝑦)) → (1o𝐶 → ((𝐶o 𝑦) ·o 1o) ∈ ((𝐶o 𝑦) ·o 𝐶)))
4640, 36, 44, 45syl21anc 836 . . . . . . . . . 10 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (1o𝐶 → ((𝐶o 𝑦) ·o 1o) ∈ ((𝐶o 𝑦) ·o 𝐶)))
4739, 46mpd 15 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ((𝐶o 𝑦) ·o 1o) ∈ ((𝐶o 𝑦) ·o 𝐶))
4838, 47eqeltrrd 2894 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ ((𝐶o 𝑦) ·o 𝐶))
49 oesuc 8139 . . . . . . . . 9 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶o suc 𝑦) = ((𝐶o 𝑦) ·o 𝐶))
5013, 49sylan 583 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o suc 𝑦) = ((𝐶o 𝑦) ·o 𝐶))
5148, 50eleqtrrd 2896 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ (𝐶o suc 𝑦))
52 suceloni 7512 . . . . . . . . 9 (𝑦 ∈ On → suc 𝑦 ∈ On)
53 oecl 8149 . . . . . . . . 9 ((𝐶 ∈ On ∧ suc 𝑦 ∈ On) → (𝐶o suc 𝑦) ∈ On)
5413, 52, 53syl2an 598 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o suc 𝑦) ∈ On)
55 ontr1 6209 . . . . . . . 8 ((𝐶o suc 𝑦) ∈ On → (((𝐶o 𝐴) ∈ (𝐶o 𝑦) ∧ (𝐶o 𝑦) ∈ (𝐶o suc 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦)))
5654, 55syl 17 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (((𝐶o 𝐴) ∈ (𝐶o 𝑦) ∧ (𝐶o 𝑦) ∈ (𝐶o suc 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦)))
5751, 56mpan2d 693 . . . . . 6 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦)))
5857expcom 417 . . . . 5 (𝑦 ∈ On → (𝐶 ∈ (On ∖ 2o) → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦))))
5958adantr 484 . . . 4 ((𝑦 ∈ On ∧ 𝐴𝑦) → (𝐶 ∈ (On ∖ 2o) → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦))))
6059a2d 29 . . 3 ((𝑦 ∈ On ∧ 𝐴𝑦) → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦))))
61 bi2.04 392 . . . . . 6 ((𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
6261ralbii 3136 . . . . 5 (∀𝑦𝑥 (𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ ∀𝑦𝑥 (𝐶 ∈ (On ∖ 2o) → (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
63 r19.21v 3145 . . . . 5 (∀𝑦𝑥 (𝐶 ∈ (On ∖ 2o) → (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) → ∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
6462, 63bitri 278 . . . 4 (∀𝑦𝑥 (𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) → ∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
65 limsuc 7548 . . . . . . . . . 10 (Lim 𝑥 → (𝐴𝑥 ↔ suc 𝐴𝑥))
6665biimpa 480 . . . . . . . . 9 ((Lim 𝑥𝐴𝑥) → suc 𝐴𝑥)
67 elex 3462 . . . . . . . . . . . . 13 (suc 𝐴𝑥 → suc 𝐴 ∈ V)
68 sucexb 7508 . . . . . . . . . . . . . 14 (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
69 sucidg 6241 . . . . . . . . . . . . . 14 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
7068, 69sylbir 238 . . . . . . . . . . . . 13 (suc 𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
7167, 70syl 17 . . . . . . . . . . . 12 (suc 𝐴𝑥𝐴 ∈ suc 𝐴)
72 eleq2 2881 . . . . . . . . . . . . . 14 (𝑦 = suc 𝐴 → (𝐴𝑦𝐴 ∈ suc 𝐴))
73 oveq2 7147 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝐴 → (𝐶o 𝑦) = (𝐶o suc 𝐴))
7473eleq2d 2878 . . . . . . . . . . . . . 14 (𝑦 = suc 𝐴 → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) ↔ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
7572, 74imbi12d 348 . . . . . . . . . . . . 13 (𝑦 = suc 𝐴 → ((𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) ↔ (𝐴 ∈ suc 𝐴 → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
7675rspcv 3569 . . . . . . . . . . . 12 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐴 ∈ suc 𝐴 → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
7771, 76mpid 44 . . . . . . . . . . 11 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
7877anc2li 559 . . . . . . . . . 10 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (suc 𝐴𝑥 ∧ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
7973eliuni 4890 . . . . . . . . . 10 ((suc 𝐴𝑥 ∧ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)) → (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦))
8078, 79syl6 35 . . . . . . . . 9 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦)))
8166, 80syl 17 . . . . . . . 8 ((Lim 𝑥𝐴𝑥) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦)))
8281adantr 484 . . . . . . 7 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦)))
8313adantl 485 . . . . . . . . . 10 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → 𝐶 ∈ On)
84 simpl 486 . . . . . . . . . 10 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → Lim 𝑥)
8523adantl 485 . . . . . . . . . 10 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → ∅ ∈ 𝐶)
86 vex 3447 . . . . . . . . . . 11 𝑥 ∈ V
87 oelim 8146 . . . . . . . . . . 11 (((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐶) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
8886, 87mpanlr1 705 . . . . . . . . . 10 (((𝐶 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐶) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
8983, 84, 85, 88syl21anc 836 . . . . . . . . 9 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
9089adantlr 714 . . . . . . . 8 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
9190eleq2d 2878 . . . . . . 7 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦)))
9282, 91sylibrd 262 . . . . . 6 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)))
9392ex 416 . . . . 5 ((Lim 𝑥𝐴𝑥) → (𝐶 ∈ (On ∖ 2o) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o 𝑥))))
9493a2d 29 . . . 4 ((Lim 𝑥𝐴𝑥) → ((𝐶 ∈ (On ∖ 2o) → ∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥))))
9564, 94syl5bi 245 . . 3 ((Lim 𝑥𝐴𝑥) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥))))
963, 6, 9, 12, 34, 60, 95tfindsg2 7560 . 2 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝐵)))
9796impancom 455 1 ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖ 2o)) → (𝐴𝐵 → (𝐶o 𝐴) ∈ (𝐶o 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ∀wral 3109  Vcvv 3444   ∖ cdif 3881  ∅c0 4246  ∪ ciun 4884  Oncon0 6163  Lim wlim 6164  suc csuc 6165  (class class class)co 7139  1oc1o 8082  2oc2o 8083   ·o comu 8087   ↑o coe 8088 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-omul 8094  df-oexp 8095 This theorem is referenced by:  oeord  8201  oecan  8202  oeworde  8206  oelimcl  8213
 Copyright terms: Public domain W3C validator