resvlemOLD

Description: Obsolete version of resvlem as of 31-Oct-2024. Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	resvlemOLD.r	$⊢ R = W ↾_{𝑣} A$
	resvlemOLD.e	$⊢ C = E (W)$
	resvlemOLD.f	$⊢ E = Slot N$
	resvlemOLD.n	$⊢ N \in ℕ$
	resvlemOLD.b	$⊢ N \neq 5$
Assertion	resvlemOLD	$⊢ A \in V \to C = E (R)$

Proof

Step	Hyp	Ref	Expression
1		resvlemOLD.r	$⊢ R = W ↾_{𝑣} A$
2		resvlemOLD.e	$⊢ C = E (W)$
3		resvlemOLD.f	$⊢ E = Slot N$
4		resvlemOLD.n	$⊢ N \in ℕ$
5		resvlemOLD.b	$⊢ N \neq 5$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
8	1 6 7	resvid2	$⊢ ({Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to R = W$
9	8	fveq2d	$⊢ ({Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W)$
10	9	3expib	$⊢ {Base}_{Scalar (W)} \subseteq A \to ((W \in V \land A \in V) \to E (R) = E (W))$
11	1 6 7	resvval2	$⊢ (\neg {Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to R = W sSet ⟨Scalar (ndx), Scalar (W) ↾_{𝑠} A⟩$
12	11	fveq2d	$⊢ (\neg {Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W sSet ⟨Scalar (ndx), Scalar (W) ↾_{𝑠} A⟩)$
13	3 4	ndxid	$⊢ E = Slot E (ndx)$
14	3 4	ndxarg	$⊢ E (ndx) = N$
15	14 5	eqnetri	$⊢ E (ndx) \neq 5$
16		scandx	$⊢ Scalar (ndx) = 5$
17	15 16	neeqtrri	$⊢ E (ndx) \neq Scalar (ndx)$
18	13 17	setsnid	$⊢ E (W) = E (W sSet ⟨Scalar (ndx), Scalar (W) ↾_{𝑠} A⟩)$
19	12 18	eqtr4di	$⊢ (\neg {Base}_{Scalar (W)} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W)$
20	19	3expib	$⊢ \neg {Base}_{Scalar (W)} \subseteq A \to ((W \in V \land A \in V) \to E (R) = E (W))$
21	10 20	pm2.61i	$⊢ (W \in V \land A \in V) \to E (R) = E (W)$
22		reldmresv	$⊢ Rel dom ↾_{𝑣}$
23	22	ovprc1	$⊢ \neg W \in V \to W ↾_{𝑣} A = \emptyset$
24	1 23	eqtrid	$⊢ \neg W \in V \to R = \emptyset$
25	24	fveq2d	$⊢ \neg W \in V \to E (R) = E (\emptyset)$
26	3	str0	$⊢ \emptyset = E (\emptyset)$
27	25 26	eqtr4di	$⊢ \neg W \in V \to E (R) = \emptyset$
28		fvprc	$⊢ \neg W \in V \to E (W) = \emptyset$
29	27 28	eqtr4d	$⊢ \neg W \in V \to E (R) = E (W)$
30	29	adantr	$⊢ (\neg W \in V \land A \in V) \to E (R) = E (W)$
31	21 30	pm2.61ian	$⊢ A \in V \to E (R) = E (W)$
32	2 31	eqtr4id	$⊢ A \in V \to C = E (R)$

Metamath Proof Explorer

Theorem resvlemOLD

Proof