Theorem 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{\upharpoonright }_{𝑠}A$$
	resslemOLD.e	$$⊢C=E\left(W\right)$$
	resslemOLD.f	$$⊢E=\mathrm{Slot}N$$
	resslemOLD.n	$$⊢N\in \mathbb{N}$$
	resslemOLD.b	$$⊢1<N$$
Assertion	resslemOLD	$$⊢A\in V\to C=E\left(R\right)$$

Proof

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