Definition df-opsr 21466

Description: Define a total order on the set of all power series in 𝑠 from the index set 𝑖 given a wellordering 𝑟 of 𝑖 and a totally ordered base ring 𝑠. (Contributed by Mario Carneiro, 8-Feb-2015.)

Assertion

Ref	Expression
df-opsr	⊢ ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩)))

Distinct variable group:   ℎ,𝑑,𝑖,𝑝,𝑟,𝑠,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-opsr

Step	Hyp	Ref	Expression
1		copws 21461	. 2 class ordPwSer
2		vi	. . 3 setvar 𝑖
3		vs	. . 3 setvar 𝑠
4		cvv 3475	. . 3 class V
5		vr	. . . 4 setvar 𝑟
6	2	cv 1541	. . . . . 6 class 𝑖
7	6, 6	cxp 5675	. . . . 5 class (𝑖 × 𝑖)
8	7	cpw 4603	. . . 4 class 𝒫 (𝑖 × 𝑖)
9		vp	. . . . 5 setvar 𝑝
10	3	cv 1541	. . . . . 6 class 𝑠
11		cmps 21457	. . . . . 6 class mPwSer
12	6, 10, 11	co 7409	. . . . 5 class (𝑖 mPwSer 𝑠)
13	9	cv 1541	. . . . . 6 class 𝑝
14		cnx 17126	. . . . . . . 8 class ndx
15		cple 17204	. . . . . . . 8 class le
16	14, 15	cfv 6544	. . . . . . 7 class (le‘ndx)
17		vx	. . . . . . . . . . . 12 setvar 𝑥
18	17	cv 1541	. . . . . . . . . . 11 class 𝑥
19		vy	. . . . . . . . . . . 12 setvar 𝑦
20	19	cv 1541	. . . . . . . . . . 11 class 𝑦
21	18, 20	cpr 4631	. . . . . . . . . 10 class {𝑥, 𝑦}
22		cbs 17144	. . . . . . . . . . 11 class Base
23	13, 22	cfv 6544	. . . . . . . . . 10 class (Base‘𝑝)
24	21, 23	wss 3949	. . . . . . . . 9 wff {𝑥, 𝑦} ⊆ (Base‘𝑝)
25		vz	. . . . . . . . . . . . . . . 16 setvar 𝑧
26	25	cv 1541	. . . . . . . . . . . . . . 15 class 𝑧
27	26, 18	cfv 6544	. . . . . . . . . . . . . 14 class (𝑥‘𝑧)
28	26, 20	cfv 6544	. . . . . . . . . . . . . 14 class (𝑦‘𝑧)
29		cplt 18261	. . . . . . . . . . . . . . 15 class lt
30	10, 29	cfv 6544	. . . . . . . . . . . . . 14 class (lt‘𝑠)
31	27, 28, 30	wbr 5149	. . . . . . . . . . . . 13 wff (𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧)
32		vw	. . . . . . . . . . . . . . . . 17 setvar 𝑤
33	32	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑤
34	5	cv 1541	. . . . . . . . . . . . . . . . 17 class 𝑟
35		cltb 21460	. . . . . . . . . . . . . . . . 17 class <bag
36	34, 6, 35	co 7409	. . . . . . . . . . . . . . . 16 class (𝑟 <bag 𝑖)
37	33, 26, 36	wbr 5149	. . . . . . . . . . . . . . 15 wff 𝑤(𝑟 <bag 𝑖)𝑧
38	33, 18	cfv 6544	. . . . . . . . . . . . . . . 16 class (𝑥‘𝑤)
39	33, 20	cfv 6544	. . . . . . . . . . . . . . . 16 class (𝑦‘𝑤)
40	38, 39	wceq 1542	. . . . . . . . . . . . . . 15 wff (𝑥‘𝑤) = (𝑦‘𝑤)
41	37, 40	wi 4	. . . . . . . . . . . . . 14 wff (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))
42		vd	. . . . . . . . . . . . . . 15 setvar 𝑑
43	42	cv 1541	. . . . . . . . . . . . . 14 class 𝑑
44	41, 32, 43	wral 3062	. . . . . . . . . . . . 13 wff ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))
45	31, 44	wa 397	. . . . . . . . . . . 12 wff ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))
46	45, 25, 43	wrex 3071	. . . . . . . . . . 11 wff ∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))
47		vh	. . . . . . . . . . . . . . . 16 setvar ℎ
48	47	cv 1541	. . . . . . . . . . . . . . 15 class ℎ
49	48	ccnv 5676	. . . . . . . . . . . . . 14 class ◡ℎ
50		cn 12212	. . . . . . . . . . . . . 14 class ℕ
51	49, 50	cima 5680	. . . . . . . . . . . . 13 class (◡ℎ “ ℕ)
52		cfn 8939	. . . . . . . . . . . . 13 class Fin
53	51, 52	wcel 2107	. . . . . . . . . . . 12 wff (◡ℎ “ ℕ) ∈ Fin
54		cn0 12472	. . . . . . . . . . . . 13 class ℕ0
55		cmap 8820	. . . . . . . . . . . . 13 class ↑m
56	54, 6, 55	co 7409	. . . . . . . . . . . 12 class (ℕ0 ↑m 𝑖)
57	53, 47, 56	crab 3433	. . . . . . . . . . 11 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
58	46, 42, 57	wsbc 3778	. . . . . . . . . 10 wff [{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))
59	17, 19	weq 1967	. . . . . . . . . 10 wff 𝑥 = 𝑦
60	58, 59	wo 846	. . . . . . . . 9 wff ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)
61	24, 60	wa 397	. . . . . . . 8 wff ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))
62	61, 17, 19	copab 5211	. . . . . . 7 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}
63	16, 62	cop 4635	. . . . . 6 class ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩
64		csts 17096	. . . . . 6 class sSet
65	13, 63, 64	co 7409	. . . . 5 class (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩)
66	9, 12, 65	csb 3894	. . . 4 class ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩)
67	5, 8, 66	cmpt 5232	. . 3 class (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩))
68	2, 3, 4, 4, 67	cmpo 7411	. 2 class (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
69	1, 68	wceq 1542	1 wff ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩)))

This definition is referenced by:  reldmopsr  21600  opsrval  21601