Theorem basprssdmsets

Description: The pair of the base index and another index is a subset of the domain of the structure obtained by replacing/adding a slot at the other index in a structure having a base slot. (Contributed by AV, 7-Jun-2021) (Revised by AV, 16-Nov-2021)

	Ref	Expression
Hypotheses	basprssdmsets.s	$$⊢\phi \to S\mathrm{Struct}X$$
	basprssdmsets.i	$$⊢\phi \to I\in U$$
	basprssdmsets.w	$$⊢\phi \to E\in W$$
	basprssdmsets.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S$$
Assertion	basprssdmsets	$$⊢\phi \to \left\{{\mathrm{Base}}_{\mathrm{ndx}},I\right\}\subseteq \mathrm{dom}\left(S\mathrm{sSet}⟨I,E⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		basprssdmsets.s	$$⊢\phi \to S\mathrm{Struct}X$$
2		basprssdmsets.i	$$⊢\phi \to I\in U$$
3		basprssdmsets.w	$$⊢\phi \to E\in W$$
4		basprssdmsets.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S$$
5	4	orcd	$$⊢\phi \to \left({\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S\vee {\mathrm{Base}}_{\mathrm{ndx}}\in \left\{I\right\}\right)$$
6		elun	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \left(\mathrm{dom}S\cup \left\{I\right\}\right)\leftrightarrow \left({\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S\vee {\mathrm{Base}}_{\mathrm{ndx}}\in \left\{I\right\}\right)$$
7	5 6	sylibr	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \left(\mathrm{dom}S\cup \left\{I\right\}\right)$$
8		snidg	$$⊢I\in U\to I\in \left\{I\right\}$$
9	2 8	syl	$$⊢\phi \to I\in \left\{I\right\}$$
10	9	olcd	$$⊢\phi \to \left(I\in \mathrm{dom}S\vee I\in \left\{I\right\}\right)$$
11		elun	$$⊢I\in \left(\mathrm{dom}S\cup \left\{I\right\}\right)\leftrightarrow \left(I\in \mathrm{dom}S\vee I\in \left\{I\right\}\right)$$
12	10 11	sylibr	$$⊢\phi \to I\in \left(\mathrm{dom}S\cup \left\{I\right\}\right)$$
13	7 12	prssd	$$⊢\phi \to \left\{{\mathrm{Base}}_{\mathrm{ndx}},I\right\}\subseteq \mathrm{dom}S\cup \left\{I\right\}$$
14		structex	$$⊢S\mathrm{Struct}X\to S\in \mathrm{V}$$
15	1 14	syl	$$⊢\phi \to S\in \mathrm{V}$$
16		setsdm	$$⊢\left(S\in \mathrm{V}\wedge E\in W\right)\to \mathrm{dom}\left(S\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}S\cup \left\{I\right\}$$
17	15 3 16	syl2anc	$$⊢\phi \to \mathrm{dom}\left(S\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}S\cup \left\{I\right\}$$
18	13 17	sseqtrrd	$$⊢\phi \to \left\{{\mathrm{Base}}_{\mathrm{ndx}},I\right\}\subseteq \mathrm{dom}\left(S\mathrm{sSet}⟨I,E⟩\right)$$