resslemOLD

Description: Obsolete version of resseqnbas as of 21-Oct-2024. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	resslemOLD.r	$⊢ R = W ↾_{𝑠} A$
	resslemOLD.e	$⊢ C = E (W)$
	resslemOLD.f	$⊢ E = Slot N$
	resslemOLD.n	$⊢ N \in ℕ$
	resslemOLD.b	$⊢ 1 < N$
Assertion	resslemOLD	$⊢ A \in V \to C = E (R)$

Proof

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

Metamath Proof Explorer

Theorem resslemOLD

Proof