Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reldmopsr | Structured version Visualization version GIF version |
Description: Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
Ref | Expression |
---|---|
reldmopsr | ⊢ Rel dom ordPwSer |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-opsr 20123 | . 2 ⊢ ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) | |
2 | 1 | reldmmpo 7271 | 1 ⊢ Rel dom ordPwSer |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3486 [wsbc 3763 ⦋csb 3871 ⊆ wss 3924 𝒫 cpw 4525 {cpr 4555 〈cop 4559 class class class wbr 5052 {copab 5114 ↦ cmpt 5132 × cxp 5539 ◡ccnv 5540 dom cdm 5541 “ cima 5544 Rel wrel 5546 ‘cfv 6341 (class class class)co 7142 ↑m cmap 8392 Fincfn 8495 ℕcn 11624 ℕ0cn0 11884 ndxcnx 16463 sSet csts 16464 Basecbs 16466 lecple 16555 ltcplt 17534 mPwSer cmps 20114 <bag cltb 20117 ordPwSer copws 20118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pr 5316 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3488 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-sn 4554 df-pr 4556 df-op 4560 df-br 5053 df-opab 5115 df-xp 5547 df-rel 5548 df-dm 5551 df-oprab 7146 df-mpo 7147 df-opsr 20123 |
This theorem is referenced by: opsrle 20239 opsrbaslem 20241 psr1val 20337 |
Copyright terms: Public domain | W3C validator |