Theorem resslem

Description: Other elements of a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	resslem.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
	resslem.e	$$⊢C=E\left(W\right)$$
	resslem.f	$$⊢E=\mathrm{Slot}N$$
	resslem.n	$$⊢N\in \mathbb{N}$$
	resslem.b	$$⊢1<N$$
Assertion	resslem	$$⊢A\in V\to C=E\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		resslem.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
2		resslem.e	$$⊢C=E\left(W\right)$$
3		resslem.f	$$⊢E=\mathrm{Slot}N$$
4		resslem.n	$$⊢N\in \mathbb{N}$$
5		resslem.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	syl6eqr	$$⊢\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	syl6eqr	$$⊢\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	32 2	syl6reqr	$$⊢A\in V\to C=E\left(R\right)$$