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

Theorem oeordi 8054
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 7015 . . . . 5 (𝑥 = suc 𝐴 → (𝐶o 𝑥) = (𝐶o suc 𝐴))
21eleq2d 2866 . . . 4 (𝑥 = suc 𝐴 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
32imbi2d 342 . . 3 (𝑥 = suc 𝐴 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
4 oveq2 7015 . . . . 5 (𝑥 = 𝑦 → (𝐶o 𝑥) = (𝐶o 𝑦))
54eleq2d 2866 . . . 4 (𝑥 = 𝑦 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o 𝑦)))
65imbi2d 342 . . 3 (𝑥 = 𝑦 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
7 oveq2 7015 . . . . 5 (𝑥 = suc 𝑦 → (𝐶o 𝑥) = (𝐶o suc 𝑦))
87eleq2d 2866 . . . 4 (𝑥 = suc 𝑦 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o suc 𝑦)))
98imbi2d 342 . . 3 (𝑥 = suc 𝑦 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦))))
10 oveq2 7015 . . . . 5 (𝑥 = 𝐵 → (𝐶o 𝑥) = (𝐶o 𝐵))
1110eleq2d 2866 . . . 4 (𝑥 = 𝐵 → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ (𝐶o 𝐵)))
1211imbi2d 342 . . 3 (𝑥 = 𝐵 → ((𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝐵))))
13 eldifi 4019 . . . . . . . 8 (𝐶 ∈ (On ∖ 2o) → 𝐶 ∈ On)
14 oecl 8004 . . . . . . . 8 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ On)
1513, 14sylan 580 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ On)
16 om1 8009 . . . . . . 7 ((𝐶o 𝐴) ∈ On → ((𝐶o 𝐴) ·o 1o) = (𝐶o 𝐴))
1715, 16syl 17 . . . . . 6 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ((𝐶o 𝐴) ·o 1o) = (𝐶o 𝐴))
18 ondif2 7969 . . . . . . . . 9 (𝐶 ∈ (On ∖ 2o) ↔ (𝐶 ∈ On ∧ 1o𝐶))
1918simprbi 497 . . . . . . . 8 (𝐶 ∈ (On ∖ 2o) → 1o𝐶)
2019adantr 481 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 1o𝐶)
2113adantr 481 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐶 ∈ On)
22 simpr 485 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐴 ∈ On)
23 dif20el 7972 . . . . . . . . . 10 (𝐶 ∈ (On ∖ 2o) → ∅ ∈ 𝐶)
2423adantr 481 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ∅ ∈ 𝐶)
25 oen0 8053 . . . . . . . . 9 (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐶) → ∅ ∈ (𝐶o 𝐴))
2621, 22, 24, 25syl21anc 834 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ∅ ∈ (𝐶o 𝐴))
27 omordi 8033 . . . . . . . 8 (((𝐶 ∈ On ∧ (𝐶o 𝐴) ∈ On) ∧ ∅ ∈ (𝐶o 𝐴)) → (1o𝐶 → ((𝐶o 𝐴) ·o 1o) ∈ ((𝐶o 𝐴) ·o 𝐶)))
2821, 15, 26, 27syl21anc 834 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (1o𝐶 → ((𝐶o 𝐴) ·o 1o) ∈ ((𝐶o 𝐴) ·o 𝐶)))
2920, 28mpd 15 . . . . . 6 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → ((𝐶o 𝐴) ·o 1o) ∈ ((𝐶o 𝐴) ·o 𝐶))
3017, 29eqeltrrd 2882 . . . . 5 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ ((𝐶o 𝐴) ·o 𝐶))
31 oesuc 7994 . . . . . 6 ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶o suc 𝐴) = ((𝐶o 𝐴) ·o 𝐶))
3213, 31sylan 580 . . . . 5 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o suc 𝐴) = ((𝐶o 𝐴) ·o 𝐶))
3330, 32eleqtrrd 2884 . . . 4 ((𝐶 ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))
3433expcom 414 . . 3 (𝐴 ∈ On → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
35 oecl 8004 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ On)
3613, 35sylan 580 . . . . . . . . . 10 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ On)
37 om1 8009 . . . . . . . . . 10 ((𝐶o 𝑦) ∈ On → ((𝐶o 𝑦) ·o 1o) = (𝐶o 𝑦))
3836, 37syl 17 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ((𝐶o 𝑦) ·o 1o) = (𝐶o 𝑦))
3919adantr 481 . . . . . . . . . 10 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → 1o𝐶)
4013adantr 481 . . . . . . . . . . 11 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → 𝐶 ∈ On)
41 simpr 485 . . . . . . . . . . . 12 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → 𝑦 ∈ On)
4223adantr 481 . . . . . . . . . . . 12 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ∅ ∈ 𝐶)
43 oen0 8053 . . . . . . . . . . . 12 (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ 𝐶) → ∅ ∈ (𝐶o 𝑦))
4440, 41, 42, 43syl21anc 834 . . . . . . . . . . 11 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ∅ ∈ (𝐶o 𝑦))
45 omordi 8033 . . . . . . . . . . 11 (((𝐶 ∈ On ∧ (𝐶o 𝑦) ∈ On) ∧ ∅ ∈ (𝐶o 𝑦)) → (1o𝐶 → ((𝐶o 𝑦) ·o 1o) ∈ ((𝐶o 𝑦) ·o 𝐶)))
4640, 36, 44, 45syl21anc 834 . . . . . . . . . 10 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (1o𝐶 → ((𝐶o 𝑦) ·o 1o) ∈ ((𝐶o 𝑦) ·o 𝐶)))
4739, 46mpd 15 . . . . . . . . 9 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ((𝐶o 𝑦) ·o 1o) ∈ ((𝐶o 𝑦) ·o 𝐶))
4838, 47eqeltrrd 2882 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ ((𝐶o 𝑦) ·o 𝐶))
49 oesuc 7994 . . . . . . . . 9 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶o suc 𝑦) = ((𝐶o 𝑦) ·o 𝐶))
5013, 49sylan 580 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o suc 𝑦) = ((𝐶o 𝑦) ·o 𝐶))
5148, 50eleqtrrd 2884 . . . . . . 7 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o 𝑦) ∈ (𝐶o suc 𝑦))
52 suceloni 7375 . . . . . . . . 9 (𝑦 ∈ On → suc 𝑦 ∈ On)
53 oecl 8004 . . . . . . . . 9 ((𝐶 ∈ On ∧ suc 𝑦 ∈ On) → (𝐶o suc 𝑦) ∈ On)
5413, 52, 53syl2an 595 . . . . . . . 8 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → (𝐶o suc 𝑦) ∈ On)
55 ontr1 6104 . . . . . . . 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 690 . . . . . 6 ((𝐶 ∈ (On ∖ 2o) ∧ 𝑦 ∈ On) → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦)))
5857expcom 414 . . . . 5 (𝑦 ∈ On → (𝐶 ∈ (On ∖ 2o) → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) → (𝐶o 𝐴) ∈ (𝐶o suc 𝑦))))
5958adantr 481 . . . 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 389 . . . . . 6 ((𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) → (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
6261ralbii 3130 . . . . 5 (∀𝑦𝑥 (𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ ∀𝑦𝑥 (𝐶 ∈ (On ∖ 2o) → (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
63 r19.21v 3140 . . . . 5 (∀𝑦𝑥 (𝐶 ∈ (On ∖ 2o) → (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) → ∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
6462, 63bitri 276 . . . 4 (∀𝑦𝑥 (𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) → ∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))))
65 limsuc 7411 . . . . . . . . . 10 (Lim 𝑥 → (𝐴𝑥 ↔ suc 𝐴𝑥))
6665biimpa 477 . . . . . . . . 9 ((Lim 𝑥𝐴𝑥) → suc 𝐴𝑥)
67 elex 3450 . . . . . . . . . . . . 13 (suc 𝐴𝑥 → suc 𝐴 ∈ V)
68 sucexb 7371 . . . . . . . . . . . . . 14 (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
69 sucidg 6136 . . . . . . . . . . . . . 14 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
7068, 69sylbir 236 . . . . . . . . . . . . 13 (suc 𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
7167, 70syl 17 . . . . . . . . . . . 12 (suc 𝐴𝑥𝐴 ∈ suc 𝐴)
72 eleq2 2869 . . . . . . . . . . . . . 14 (𝑦 = suc 𝐴 → (𝐴𝑦𝐴 ∈ suc 𝐴))
73 oveq2 7015 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝐴 → (𝐶o 𝑦) = (𝐶o suc 𝐴))
7473eleq2d 2866 . . . . . . . . . . . . . 14 (𝑦 = suc 𝐴 → ((𝐶o 𝐴) ∈ (𝐶o 𝑦) ↔ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
7572, 74imbi12d 346 . . . . . . . . . . . . 13 (𝑦 = suc 𝐴 → ((𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) ↔ (𝐴 ∈ suc 𝐴 → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
7675rspcv 3550 . . . . . . . . . . . 12 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐴 ∈ suc 𝐴 → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
7771, 76mpid 44 . . . . . . . . . . 11 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o suc 𝐴)))
7877anc2li 556 . . . . . . . . . 10 (suc 𝐴𝑥 → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (suc 𝐴𝑥 ∧ (𝐶o 𝐴) ∈ (𝐶o suc 𝐴))))
7973eliuni 4825 . . . . . . . . . 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 481 . . . . . . 7 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦)))
8313adantl 482 . . . . . . . . . 10 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → 𝐶 ∈ On)
84 simpl 483 . . . . . . . . . 10 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → Lim 𝑥)
8523adantl 482 . . . . . . . . . 10 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → ∅ ∈ 𝐶)
86 vex 3435 . . . . . . . . . . 11 𝑥 ∈ V
87 oelim 8001 . . . . . . . . . . 11 (((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐶) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
8886, 87mpanlr1 702 . . . . . . . . . 10 (((𝐶 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐶) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
8983, 84, 85, 88syl21anc 834 . . . . . . . . 9 ((Lim 𝑥𝐶 ∈ (On ∖ 2o)) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
9089adantlr 711 . . . . . . . 8 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → (𝐶o 𝑥) = 𝑦𝑥 (𝐶o 𝑦))
9190eleq2d 2866 . . . . . . 7 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → ((𝐶o 𝐴) ∈ (𝐶o 𝑥) ↔ (𝐶o 𝐴) ∈ 𝑦𝑥 (𝐶o 𝑦)))
9282, 91sylibrd 260 . . . . . 6 (((Lim 𝑥𝐴𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o 𝑥)))
9392ex 413 . . . . 5 ((Lim 𝑥𝐴𝑥) → (𝐶 ∈ (On ∖ 2o) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦)) → (𝐶o 𝐴) ∈ (𝐶o 𝑥))))
9493a2d 29 . . . 4 ((Lim 𝑥𝐴𝑥) → ((𝐶 ∈ (On ∖ 2o) → ∀𝑦𝑥 (𝐴𝑦 → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥))))
9564, 94syl5bi 243 . . 3 ((Lim 𝑥𝐴𝑥) → (∀𝑦𝑥 (𝐴𝑦 → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑦))) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝑥))))
963, 6, 9, 12, 34, 60, 95tfindsg2 7423 . 2 ((𝐵 ∈ On ∧ 𝐴𝐵) → (𝐶 ∈ (On ∖ 2o) → (𝐶o 𝐴) ∈ (𝐶o 𝐵)))
9796impancom 452 1 ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖ 2o)) → (𝐴𝐵 → (𝐶o 𝐴) ∈ (𝐶o 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1520  wcel 2079  wral 3103  Vcvv 3432  cdif 3851  c0 4206   ciun 4819  Oncon0 6058  Lim wlim 6059  suc csuc 6060  (class class class)co 7007  1oc1o 7937  2oc2o 7938   ·o comu 7942  o coe 7943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-rep 5075  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-pred 6015  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-ov 7010  df-oprab 7011  df-mpo 7012  df-om 7428  df-wrecs 7789  df-recs 7851  df-rdg 7889  df-1o 7944  df-2o 7945  df-oadd 7948  df-omul 7949  df-oexp 7950
This theorem is referenced by:  oeord  8055  oecan  8056  oeworde  8060  oelimcl  8067
  Copyright terms: Public domain W3C validator