Theorem ressval3d

Description: Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020) (Revised by AV, 3-Jul-2022) (Proof shortened by AV, 17-Oct-2024)

	Ref	Expression
Hypotheses	ressval3d.r	$$⊢R=S{\upharpoonright }_{𝑠}A$$
	ressval3d.b	$$⊢B={\mathrm{Base}}_S$$
	ressval3d.e	$$⊢E={\mathrm{Base}}_{\mathrm{ndx}}$$
	ressval3d.s	$$⊢\phi \to S\in V$$
	ressval3d.f	$$⊢\phi \to \mathrm{Fun}S$$
	ressval3d.d	$$⊢\phi \to E\in \mathrm{dom}S$$
	ressval3d.u	$$⊢\phi \to A\subseteq B$$
Assertion	ressval3d	$$⊢\phi \to R=S\mathrm{sSet}⟨E,A⟩$$

Proof

Step	Hyp	Ref	Expression
1		ressval3d.r	$$⊢R=S{\upharpoonright }_{𝑠}A$$
2		ressval3d.b	$$⊢B={\mathrm{Base}}_S$$
3		ressval3d.e	$$⊢E={\mathrm{Base}}_{\mathrm{ndx}}$$
4		ressval3d.s	$$⊢\phi \to S\in V$$
5		ressval3d.f	$$⊢\phi \to \mathrm{Fun}S$$
6		ressval3d.d	$$⊢\phi \to E\in \mathrm{dom}S$$
7		ressval3d.u	$$⊢\phi \to A\subseteq B$$
8		sspss	$$⊢A\subseteq B\leftrightarrow \left(A\subset B\vee A=B\right)$$
9		dfpss3	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg B\subseteq A\right)$$
10	9	orbi1i	$$⊢\left(A\subset B\vee A=B\right)\leftrightarrow \left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\vee A=B\right)$$
11	8 10	bitri	$$⊢A\subseteq B\leftrightarrow \left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\vee A=B\right)$$
12		simplr	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to \neg B\subseteq A$$
13	4	adantl	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to S\in V$$
14		simpl	$$⊢\left(A\subseteq B\wedge \neg B\subseteq A\right)\to A\subseteq B$$
15	2	fvexi	$$⊢B\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to B\in \mathrm{V}$$
17		ssexg	$$⊢\left(A\subseteq B\wedge B\in \mathrm{V}\right)\to A\in \mathrm{V}$$
18	14 16 17	syl2an	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to A\in \mathrm{V}$$
19	1 2	ressval2	$$⊢\left(\neg B\subseteq A\wedge S\in V\wedge A\in \mathrm{V}\right)\to R=S\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
20	12 13 18 19	syl3anc	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to R=S\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
21	3	a1i	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to E={\mathrm{Base}}_{\mathrm{ndx}}$$
22		dfss2	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
23	22	biimpi	$$⊢A\subseteq B\to A\cap B=A$$
24	23	eqcomd	$$⊢A\subseteq B\to A=A\cap B$$
25	24	adantr	$$⊢\left(A\subseteq B\wedge \neg B\subseteq A\right)\to A=A\cap B$$
26	25	adantr	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to A=A\cap B$$
27	21 26	opeq12d	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to ⟨E,A⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
28	27	eqcomd	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩=⟨E,A⟩$$
29	28	oveq2d	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to S\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩=S\mathrm{sSet}⟨E,A⟩$$
30	20 29	eqtrd	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\wedge \phi \right)\to R=S\mathrm{sSet}⟨E,A⟩$$
31	30	ex	$$⊢\left(A\subseteq B\wedge \neg B\subseteq A\right)\to \left(\phi \to R=S\mathrm{sSet}⟨E,A⟩\right)$$
32	1	a1i	$$⊢\left(A=B\wedge \phi \right)\to R=S{\upharpoonright }_{𝑠}A$$
33		oveq2	$$⊢A=B\to S{\upharpoonright }_{𝑠}A=S{\upharpoonright }_{𝑠}B$$
34	33	adantr	$$⊢\left(A=B\wedge \phi \right)\to S{\upharpoonright }_{𝑠}A=S{\upharpoonright }_{𝑠}B$$
35	4	adantl	$$⊢\left(A=B\wedge \phi \right)\to S\in V$$
36	2	ressid	$$⊢S\in V\to S{\upharpoonright }_{𝑠}B=S$$
37	35 36	syl	$$⊢\left(A=B\wedge \phi \right)\to S{\upharpoonright }_{𝑠}B=S$$
38	32 34 37	3eqtrd	$$⊢\left(A=B\wedge \phi \right)\to R=S$$
39		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
40	3 6	eqeltrrid	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S$$
41	39 4 5 40	setsidvald	$$⊢\phi \to S=S\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩$$
42	41	adantl	$$⊢\left(A=B\wedge \phi \right)\to S=S\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩$$
43	3	a1i	$$⊢\left(A=B\wedge \phi \right)\to E={\mathrm{Base}}_{\mathrm{ndx}}$$
44		simpl	$$⊢\left(A=B\wedge \phi \right)\to A=B$$
45	44 2	eqtrdi	$$⊢\left(A=B\wedge \phi \right)\to A={\mathrm{Base}}_S$$
46	43 45	opeq12d	$$⊢\left(A=B\wedge \phi \right)\to ⟨E,A⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩$$
47	46	eqcomd	$$⊢\left(A=B\wedge \phi \right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩=⟨E,A⟩$$
48	47	oveq2d	$$⊢\left(A=B\wedge \phi \right)\to S\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩=S\mathrm{sSet}⟨E,A⟩$$
49	38 42 48	3eqtrd	$$⊢\left(A=B\wedge \phi \right)\to R=S\mathrm{sSet}⟨E,A⟩$$
50	49	ex	$$⊢A=B\to \left(\phi \to R=S\mathrm{sSet}⟨E,A⟩\right)$$
51	31 50	jaoi	$$⊢\left(\left(A\subseteq B\wedge \neg B\subseteq A\right)\vee A=B\right)\to \left(\phi \to R=S\mathrm{sSet}⟨E,A⟩\right)$$
52	11 51	sylbi	$$⊢A\subseteq B\to \left(\phi \to R=S\mathrm{sSet}⟨E,A⟩\right)$$
53	7 52	mpcom	$$⊢\phi \to R=S\mathrm{sSet}⟨E,A⟩$$