opsrval

Description: The value of the "ordered power series" function. This is the same as mPwSer psrval , but with the addition of a well-order on I we can turn a strict order on R into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	opsrval.s	$⊢ S = I mPwSer R$
	opsrval.o	$⊢ O = (I ordPwSer R) (T)$
	opsrval.b	$⊢ B = {Base}_{S}$
	opsrval.q	$⊢ \underset{˙}{<} = <_{R}$
	opsrval.c	$⊢ C = T <_{bag} I$
	opsrval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	opsrval.l	$⊢ \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
	opsrval.i	$⊢ φ \to I \in V$
	opsrval.r	$⊢ φ \to R \in W$
	opsrval.t	$⊢ φ \to T \subseteq I \times I$
Assertion	opsrval	$⊢ φ \to O = S sSet ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$

Proof

Step	Hyp	Ref	Expression
1		opsrval.s	$⊢ S = I mPwSer R$
2		opsrval.o	$⊢ O = (I ordPwSer R) (T)$
3		opsrval.b	$⊢ B = {Base}_{S}$
4		opsrval.q	$⊢ \underset{˙}{<} = <_{R}$
5		opsrval.c	$⊢ C = T <_{bag} I$
6		opsrval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
7		opsrval.l	$⊢ \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
8		opsrval.i	$⊢ φ \to I \in V$
9		opsrval.r	$⊢ φ \to R \in W$
10		opsrval.t	$⊢ φ \to T \subseteq I \times I$
11	8	elexd	$⊢ φ \to I \in V$
12	9	elexd	$⊢ φ \to R \in V$
13	8 8	xpexd	$⊢ φ \to I \times I \in V$
14		pwexg	$⊢ I \times I \in V \to 𝒫 (I \times I) \in V$
15		mptexg	$⊢ 𝒫 (I \times I) \in V \to (r \in 𝒫 (I \times I) ⟼ S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩) \in V$
16	13 14 15	3syl	$⊢ φ \to (r \in 𝒫 (I \times I) ⟼ S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩) \in V$
17		simpl	$⊢ (i = I \land s = R) \to i = I$
18	17	sqxpeqd	$⊢ (i = I \land s = R) \to i \times i = I \times I$
19	18	pweqd	$⊢ (i = I \land s = R) \to 𝒫 (i \times i) = 𝒫 (I \times I)$
20		ovexd	$⊢ (i = I \land s = R) \to i mPwSer s \in V$
21		id	$⊢ p = i mPwSer s \to p = i mPwSer s$
22		oveq12	$⊢ (i = I \land s = R) \to i mPwSer s = I mPwSer R$
23	21 22	sylan9eqr	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to p = I mPwSer R$
24	23 1	eqtr4di	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to p = S$
25	24	fveq2d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to {Base}_{p} = {Base}_{S}$
26	25 3	eqtr4di	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to {Base}_{p} = B$
27	26	sseq2d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to (\{x, y\} \subseteq {Base}_{p} \leftrightarrow \{x, y\} \subseteq B)$
28		ovex	$⊢ {ℕ_{0}}^{i} \in V$
29	28	rabex	$⊢ \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \in V$
30	29	a1i	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \in V$
31	17	adantr	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to i = I$
32	31	oveq2d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to {ℕ_{0}}^{i} = {ℕ_{0}}^{I}$
33		rabeq	$⊢ {ℕ_{0}}^{i} = {ℕ_{0}}^{I} \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
34	32 33	syl	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
35	34 6	eqtr4di	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = D$
36		simpr	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to d = D$
37		simpllr	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to s = R$
38	37	fveq2d	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to <_{s} = <_{R}$
39	38 4	eqtr4di	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to <_{s} = \underset{˙}{<}$
40	39	breqd	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to (x (z) <_{s} y (z) \leftrightarrow x (z) \underset{˙}{<} y (z))$
41	31	adantr	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to i = I$
42	41	oveq2d	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to r <_{bag} i = r <_{bag} I$
43	42	breqd	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to (w (r <_{bag} i) z \leftrightarrow w (r <_{bag} I) z)$
44	43	imbi1d	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to ((w (r <_{bag} i) z \to x (w) = y (w)) \leftrightarrow (w (r <_{bag} I) z \to x (w) = y (w)))$
45	36 44	raleqbidv	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to (\forall w \in d (w (r <_{bag} i) z \to x (w) = y (w)) \leftrightarrow \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w)))$
46	40 45	anbi12d	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to ((x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \leftrightarrow (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))))$
47	36 46	rexeqbidv	$⊢ (((i = I \land s = R) \land p = i mPwSer s) \land d = D) \to (\exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \leftrightarrow \exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))))$
48	30 35 47	sbcied2	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \leftrightarrow \exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))))$
49	48	orbi1d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to ((\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y) \leftrightarrow (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))$
50	27 49	anbi12d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to ((\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y)) \leftrightarrow (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y)))$
51	50	opabbidv	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y))\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}$
52	51	opeq2d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y))\}⟩ = ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩$
53	24 52	oveq12d	$⊢ ((i = I \land s = R) \land p = i mPwSer s) \to p sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y))\}⟩ = S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩$
54	20 53	csbied	$⊢ (i = I \land s = R) \to ⦋ (i mPwSer s) / p ⦌ (p sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y))\}⟩) = S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩$
55	19 54	mpteq12dv	$⊢ (i = I \land s = R) \to (r \in 𝒫 (i \times i) ⟼ ⦋ (i mPwSer s) / p ⦌ (p sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y))\}⟩)) = (r \in 𝒫 (I \times I) ⟼ S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩)$
56		df-opsr	$⊢ ordPwSer = (i \in V, s \in V ⟼ (r \in 𝒫 (i \times i) ⟼ ⦋ (i mPwSer s) / p ⦌ (p sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{p} \land (\underset{˙}{[} \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d \underset{˙}{]} \exists z \in d (x (z) <_{s} y (z) \land \forall w \in d (w (r <_{bag} i) z \to x (w) = y (w))) \lor x = y))\}⟩)))$
57	55 56	ovmpoga	$⊢ (I \in V \land R \in V \land (r \in 𝒫 (I \times I) ⟼ S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩) \in V) \to I ordPwSer R = (r \in 𝒫 (I \times I) ⟼ S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩)$
58	11 12 16 57	syl3anc	$⊢ φ \to I ordPwSer R = (r \in 𝒫 (I \times I) ⟼ S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩)$
59		simpr	$⊢ (φ \land r = T) \to r = T$
60	59	oveq1d	$⊢ (φ \land r = T) \to r <_{bag} I = T <_{bag} I$
61	60 5	eqtr4di	$⊢ (φ \land r = T) \to r <_{bag} I = C$
62	61	breqd	$⊢ (φ \land r = T) \to (w (r <_{bag} I) z \leftrightarrow w C z)$
63	62	imbi1d	$⊢ (φ \land r = T) \to ((w (r <_{bag} I) z \to x (w) = y (w)) \leftrightarrow (w C z \to x (w) = y (w)))$
64	63	ralbidv	$⊢ (φ \land r = T) \to (\forall w \in D (w (r <_{bag} I) z \to x (w) = y (w)) \leftrightarrow \forall w \in D (w C z \to x (w) = y (w)))$
65	64	anbi2d	$⊢ (φ \land r = T) \to ((x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \leftrightarrow (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))))$
66	65	rexbidv	$⊢ (φ \land r = T) \to (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \leftrightarrow \exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))))$
67	66	orbi1d	$⊢ (φ \land r = T) \to ((\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y) \leftrightarrow (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))$
68	67	anbi2d	$⊢ (φ \land r = T) \to ((\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y)) \leftrightarrow (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y)))$
69	68	opabbidv	$⊢ (φ \land r = T) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
70	69 7	eqtr4di	$⊢ (φ \land r = T) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\} = \underset{˙}{\leq}$
71	70	opeq2d	$⊢ (φ \land r = T) \to ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩ = ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
72	71	oveq2d	$⊢ (φ \land r = T) \to S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w (r <_{bag} I) z \to x (w) = y (w))) \lor x = y))\}⟩ = S sSet ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
73	13 10	sselpwd	$⊢ φ \to T \in 𝒫 (I \times I)$
74		ovexd	$⊢ φ \to S sSet ⟨\leq_{ndx}, \underset{˙}{\leq}⟩ \in V$
75	58 72 73 74	fvmptd	$⊢ φ \to (I ordPwSer R) (T) = S sSet ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
76	2 75	syl5eq	$⊢ φ \to O = S sSet ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$

Metamath Proof Explorer

Theorem opsrval

Proof