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

Theorem infxpenc2 9965
Description: Existence form of infxpenc 9961. A "uniform" or "canonical" version of infxpen 9957, asserting the existence of a single function 𝑔 that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015.)
Assertion
Ref Expression
infxpenc2 (𝐴 ∈ On β†’ βˆƒπ‘”βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ (π‘”β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
Distinct variable group:   𝑔,𝑏,𝐴

Proof of Theorem infxpenc2
Dummy variables 𝑓 𝑛 𝑀 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnfcom3c 9649 . 2 (𝐴 ∈ On β†’ βˆƒπ‘›βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)))
2 df-2o 8418 . . . . . . . 8 2o = suc 1o
32oveq2i 7373 . . . . . . 7 (Ο‰ ↑o 2o) = (Ο‰ ↑o suc 1o)
4 omelon 9589 . . . . . . . 8 Ο‰ ∈ On
5 1on 8429 . . . . . . . 8 1o ∈ On
6 oesuc 8478 . . . . . . . 8 ((Ο‰ ∈ On ∧ 1o ∈ On) β†’ (Ο‰ ↑o suc 1o) = ((Ο‰ ↑o 1o) Β·o Ο‰))
74, 5, 6mp2an 691 . . . . . . 7 (Ο‰ ↑o suc 1o) = ((Ο‰ ↑o 1o) Β·o Ο‰)
8 oe1 8496 . . . . . . . . 9 (Ο‰ ∈ On β†’ (Ο‰ ↑o 1o) = Ο‰)
94, 8ax-mp 5 . . . . . . . 8 (Ο‰ ↑o 1o) = Ο‰
109oveq1i 7372 . . . . . . 7 ((Ο‰ ↑o 1o) Β·o Ο‰) = (Ο‰ Β·o Ο‰)
113, 7, 103eqtri 2769 . . . . . 6 (Ο‰ ↑o 2o) = (Ο‰ Β·o Ο‰)
12 omxpen 9025 . . . . . . 7 ((Ο‰ ∈ On ∧ Ο‰ ∈ On) β†’ (Ο‰ Β·o Ο‰) β‰ˆ (Ο‰ Γ— Ο‰))
134, 4, 12mp2an 691 . . . . . 6 (Ο‰ Β·o Ο‰) β‰ˆ (Ο‰ Γ— Ο‰)
1411, 13eqbrtri 5131 . . . . 5 (Ο‰ ↑o 2o) β‰ˆ (Ο‰ Γ— Ο‰)
15 xpomen 9958 . . . . 5 (Ο‰ Γ— Ο‰) β‰ˆ Ο‰
1614, 15entri 8955 . . . 4 (Ο‰ ↑o 2o) β‰ˆ Ο‰
1716a1i 11 . . 3 (𝐴 ∈ On β†’ (Ο‰ ↑o 2o) β‰ˆ Ο‰)
18 bren 8900 . . 3 ((Ο‰ ↑o 2o) β‰ˆ Ο‰ ↔ βˆƒπ‘“ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)
1917, 18sylib 217 . 2 (𝐴 ∈ On β†’ βˆƒπ‘“ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)
20 exdistrv 1960 . . 3 (βˆƒπ‘›βˆƒπ‘“(βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰) ↔ (βˆƒπ‘›βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ βˆƒπ‘“ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰))
21 simpl 484 . . . . . 6 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ 𝐴 ∈ On)
22 simprl 770 . . . . . . 7 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)))
23 sseq2 3975 . . . . . . . . 9 (π‘₯ = 𝑏 β†’ (Ο‰ βŠ† π‘₯ ↔ Ο‰ βŠ† 𝑏))
24 oveq2 7370 . . . . . . . . . . . 12 (𝑦 = 𝑀 β†’ (Ο‰ ↑o 𝑦) = (Ο‰ ↑o 𝑀))
2524f1oeq3d 6786 . . . . . . . . . . 11 (𝑦 = 𝑀 β†’ ((π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦) ↔ (π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
2625cbvrexvw 3229 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦) ↔ βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀))
27 fveq2 6847 . . . . . . . . . . . . 13 (π‘₯ = 𝑏 β†’ (π‘›β€˜π‘₯) = (π‘›β€˜π‘))
2827f1oeq1d 6784 . . . . . . . . . . . 12 (π‘₯ = 𝑏 β†’ ((π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀) ↔ (π‘›β€˜π‘):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
29 f1oeq2 6778 . . . . . . . . . . . 12 (π‘₯ = 𝑏 β†’ ((π‘›β€˜π‘):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀) ↔ (π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
3028, 29bitrd 279 . . . . . . . . . . 11 (π‘₯ = 𝑏 β†’ ((π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀) ↔ (π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
3130rexbidv 3176 . . . . . . . . . 10 (π‘₯ = 𝑏 β†’ (βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑀) ↔ βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
3226, 31bitrid 283 . . . . . . . . 9 (π‘₯ = 𝑏 β†’ (βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦) ↔ βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
3323, 32imbi12d 345 . . . . . . . 8 (π‘₯ = 𝑏 β†’ ((Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ↔ (Ο‰ βŠ† 𝑏 β†’ βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀))))
3433cbvralvw 3228 . . . . . . 7 (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ↔ βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
3522, 34sylib 217 . . . . . 6 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ βˆƒπ‘€ ∈ (On βˆ– 1o)(π‘›β€˜π‘):𝑏–1-1-ontoβ†’(Ο‰ ↑o 𝑀)))
36 oveq2 7370 . . . . . . . . 9 (𝑏 = 𝑧 β†’ (Ο‰ ↑o 𝑏) = (Ο‰ ↑o 𝑧))
3736cbvmptv 5223 . . . . . . . 8 (𝑏 ∈ (On βˆ– 1o) ↦ (Ο‰ ↑o 𝑏)) = (𝑧 ∈ (On βˆ– 1o) ↦ (Ο‰ ↑o 𝑧))
3837cnveqi 5835 . . . . . . 7 β—‘(𝑏 ∈ (On βˆ– 1o) ↦ (Ο‰ ↑o 𝑏)) = β—‘(𝑧 ∈ (On βˆ– 1o) ↦ (Ο‰ ↑o 𝑧))
3938fveq1i 6848 . . . . . 6 (β—‘(𝑏 ∈ (On βˆ– 1o) ↦ (Ο‰ ↑o 𝑏))β€˜ran (π‘›β€˜π‘)) = (β—‘(𝑧 ∈ (On βˆ– 1o) ↦ (Ο‰ ↑o 𝑧))β€˜ran (π‘›β€˜π‘))
40 2on 8431 . . . . . . . . . 10 2o ∈ On
41 peano1 7830 . . . . . . . . . . 11 βˆ… ∈ Ο‰
42 oen0 8538 . . . . . . . . . . 11 (((Ο‰ ∈ On ∧ 2o ∈ On) ∧ βˆ… ∈ Ο‰) β†’ βˆ… ∈ (Ο‰ ↑o 2o))
4341, 42mpan2 690 . . . . . . . . . 10 ((Ο‰ ∈ On ∧ 2o ∈ On) β†’ βˆ… ∈ (Ο‰ ↑o 2o))
444, 40, 43mp2an 691 . . . . . . . . 9 βˆ… ∈ (Ο‰ ↑o 2o)
45 eqid 2737 . . . . . . . . . 10 (𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©})) = (𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©}))
4645fveqf1o 7254 . . . . . . . . 9 ((𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰ ∧ βˆ… ∈ (Ο‰ ↑o 2o) ∧ βˆ… ∈ Ο‰) β†’ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©})):(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰ ∧ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©}))β€˜βˆ…) = βˆ…))
4744, 41, 46mp3an23 1454 . . . . . . . 8 (𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰ β†’ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©})):(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰ ∧ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©}))β€˜βˆ…) = βˆ…))
4847ad2antll 728 . . . . . . 7 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©})):(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰ ∧ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©}))β€˜βˆ…) = βˆ…))
4948simpld 496 . . . . . 6 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ (𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©})):(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)
5048simprd 497 . . . . . 6 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ ((𝑓 ∘ (( I β†Ύ ((Ο‰ ↑o 2o) βˆ– {βˆ…, (β—‘π‘“β€˜βˆ…)})) βˆͺ {βŸ¨βˆ…, (β—‘π‘“β€˜βˆ…)⟩, ⟨(β—‘π‘“β€˜βˆ…), βˆ…βŸ©}))β€˜βˆ…) = βˆ…)
5121, 35, 39, 49, 50infxpenc2lem3 9964 . . . . 5 ((𝐴 ∈ On ∧ (βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰)) β†’ βˆƒπ‘”βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ (π‘”β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
5251ex 414 . . . 4 (𝐴 ∈ On β†’ ((βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰) β†’ βˆƒπ‘”βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ (π‘”β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏)))
5352exlimdvv 1938 . . 3 (𝐴 ∈ On β†’ (βˆƒπ‘›βˆƒπ‘“(βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰) β†’ βˆƒπ‘”βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ (π‘”β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏)))
5420, 53biimtrrid 242 . 2 (𝐴 ∈ On β†’ ((βˆƒπ‘›βˆ€π‘₯ ∈ 𝐴 (Ο‰ βŠ† π‘₯ β†’ βˆƒπ‘¦ ∈ (On βˆ– 1o)(π‘›β€˜π‘₯):π‘₯–1-1-ontoβ†’(Ο‰ ↑o 𝑦)) ∧ βˆƒπ‘“ 𝑓:(Ο‰ ↑o 2o)–1-1-ontoβ†’Ο‰) β†’ βˆƒπ‘”βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ (π‘”β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏)))
551, 19, 54mp2and 698 1 (𝐴 ∈ On β†’ βˆƒπ‘”βˆ€π‘ ∈ 𝐴 (Ο‰ βŠ† 𝑏 β†’ (π‘”β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074   βˆ– cdif 3912   βˆͺ cun 3913   βŠ† wss 3915  βˆ…c0 4287  {cpr 4593  βŸ¨cop 4597   class class class wbr 5110   ↦ cmpt 5193   I cid 5535   Γ— cxp 5636  β—‘ccnv 5637  ran crn 5639   β†Ύ cres 5640   ∘ ccom 5642  Oncon0 6322  suc csuc 6324  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  (class class class)co 7362  Ο‰com 7807  1oc1o 8410  2oc2o 8411   Β·o comu 8415   ↑o coe 8416   β‰ˆ cen 8887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-seqom 8399  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-oexp 8423  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-oi 9453  df-cnf 9605  df-card 9882
This theorem is referenced by:  pwfseq  10607
  Copyright terms: Public domain W3C validator