opsrbaslem

Description: Get a component of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 2-Oct-2015) (Revised by AV, 9-Sep-2021) (Revised by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	opsrbas.s	$⊢ S = I mPwSer R$
	opsrbas.o	$⊢ O = (I ordPwSer R) (T)$
	opsrbas.t	$⊢ φ \to T \subseteq I \times I$
	opsrbaslem.1	$⊢ E = Slot E (ndx)$
	opsrbaslem.2	$⊢ E (ndx) \neq \leq_{ndx}$
Assertion	opsrbaslem	$⊢ φ \to E (S) = E (O)$

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	$⊢ S = I mPwSer R$
2		opsrbas.o	$⊢ O = (I ordPwSer R) (T)$
3		opsrbas.t	$⊢ φ \to T \subseteq I \times I$
4		opsrbaslem.1	$⊢ E = Slot E (ndx)$
5		opsrbaslem.2	$⊢ E (ndx) \neq \leq_{ndx}$
6	4 5	setsnid	$⊢ E (S) = E (S sSet ⟨\leq_{ndx}, \leq_{O}⟩)$
7		eqid	$⊢ \leq_{O} = \leq_{O}$
8		simprl	$⊢ (φ \land (I \in V \land R \in V)) \to I \in V$
9		simprr	$⊢ (φ \land (I \in V \land R \in V)) \to R \in V$
10	3	adantr	$⊢ (φ \land (I \in V \land R \in V)) \to T \subseteq I \times I$
11	1 2 7 8 9 10	opsrval2	$⊢ (φ \land (I \in V \land R \in V)) \to O = S sSet ⟨\leq_{ndx}, \leq_{O}⟩$
12	11	fveq2d	$⊢ (φ \land (I \in V \land R \in V)) \to E (O) = E (S sSet ⟨\leq_{ndx}, \leq_{O}⟩)$
13	6 12	eqtr4id	$⊢ (φ \land (I \in V \land R \in V)) \to E (S) = E (O)$
14		0fv	$⊢ \emptyset (T) = \emptyset$
15	14	eqcomi	$⊢ \emptyset = \emptyset (T)$
16		reldmpsr	$⊢ Rel dom mPwSer$
17	16	ovprc	$⊢ \neg (I \in V \land R \in V) \to I mPwSer R = \emptyset$
18		reldmopsr	$⊢ Rel dom ordPwSer$
19	18	ovprc	$⊢ \neg (I \in V \land R \in V) \to I ordPwSer R = \emptyset$
20	19	fveq1d	$⊢ \neg (I \in V \land R \in V) \to (I ordPwSer R) (T) = \emptyset (T)$
21	15 17 20	3eqtr4a	$⊢ \neg (I \in V \land R \in V) \to I mPwSer R = (I ordPwSer R) (T)$
22	21 1 2	3eqtr4g	$⊢ \neg (I \in V \land R \in V) \to S = O$
23	22	fveq2d	$⊢ \neg (I \in V \land R \in V) \to E (S) = E (O)$
24	23	adantl	$⊢ (φ \land \neg (I \in V \land R \in V)) \to E (S) = E (O)$
25	13 24	pm2.61dan	$⊢ φ \to E (S) = E (O)$

Metamath Proof Explorer

Theorem opsrbaslem

Proof