Theorem setsnidel

Description: The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Hypotheses	setsidel.s	$$⊢\phi \to S\in V$$
	setsidel.b	$$⊢\phi \to B\in W$$
	setsidel.r	$$⊢R=S\mathrm{sSet}⟨A,B⟩$$
	setsnidel.c	$$⊢\phi \to C\in X$$
	setsnidel.d	$$⊢\phi \to D\in Y$$
	setsnidel.s	$$⊢\phi \to ⟨C,D⟩\in S$$
	setsnidel.n	$$⊢\phi \to A\ne C$$
Assertion	setsnidel	$$⊢\phi \to ⟨C,D⟩\in R$$

Proof

Step	Hyp	Ref	Expression
1		setsidel.s	$$⊢\phi \to S\in V$$
2		setsidel.b	$$⊢\phi \to B\in W$$
3		setsidel.r	$$⊢R=S\mathrm{sSet}⟨A,B⟩$$
4		setsnidel.c	$$⊢\phi \to C\in X$$
5		setsnidel.d	$$⊢\phi \to D\in Y$$
6		setsnidel.s	$$⊢\phi \to ⟨C,D⟩\in S$$
7		setsnidel.n	$$⊢\phi \to A\ne C$$
8	4	elexd	$$⊢\phi \to C\in \mathrm{V}$$
9	7	necomd	$$⊢\phi \to C\ne A$$
10		eldifsn	$$⊢C\in \left(\mathrm{V}\setminus \left\{A\right\}\right)\leftrightarrow \left(C\in \mathrm{V}\wedge C\ne A\right)$$
11	8 9 10	sylanbrc	$$⊢\phi \to C\in \left(\mathrm{V}\setminus \left\{A\right\}\right)$$
12		opelres	$$⊢D\in Y\to \left(⟨C,D⟩\in \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\leftrightarrow \left(C\in \left(\mathrm{V}\setminus \left\{A\right\}\right)\wedge ⟨C,D⟩\in S\right)\right)$$
13	5 12	syl	$$⊢\phi \to \left(⟨C,D⟩\in \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\leftrightarrow \left(C\in \left(\mathrm{V}\setminus \left\{A\right\}\right)\wedge ⟨C,D⟩\in S\right)\right)$$
14	11 6 13	mpbir2and	$$⊢\phi \to ⟨C,D⟩\in \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)$$
15		elun1	$$⊢⟨C,D⟩\in \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\to ⟨C,D⟩\in \left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)$$
16	14 15	syl	$$⊢\phi \to ⟨C,D⟩\in \left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)$$
17		setsval	$$⊢\left(S\in V\wedge B\in W\right)\to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
18	1 2 17	syl2anc	$$⊢\phi \to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
19	3 18	syl5eq	$$⊢\phi \to R=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
20	16 19	eleqtrrd	$$⊢\phi \to ⟨C,D⟩\in R$$