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	|- ( ph -> S Struct X )
	basprssdmsets.i	|- ( ph -> I e. U )
	basprssdmsets.w	|- ( ph -> E e. W )
	basprssdmsets.b	|- ( ph -> ( Base ` ndx ) e. dom S )
Assertion	basprssdmsets	|- ( ph -> { ( Base ` ndx ) , I } C_ dom ( S sSet <. I , E >. ) )

Proof

Step	Hyp	Ref	Expression
1		basprssdmsets.s	|- ( ph -> S Struct X )
2		basprssdmsets.i	|- ( ph -> I e. U )
3		basprssdmsets.w	|- ( ph -> E e. W )
4		basprssdmsets.b	|- ( ph -> ( Base ` ndx ) e. dom S )
5	4	orcd	|- ( ph -> ( ( Base ` ndx ) e. dom S \/ ( Base ` ndx ) e. { I } ) )
6		elun	|- ( ( Base ` ndx ) e. ( dom S u. { I } ) <-> ( ( Base ` ndx ) e. dom S \/ ( Base ` ndx ) e. { I } ) )
7	5 6	sylibr	|- ( ph -> ( Base ` ndx ) e. ( dom S u. { I } ) )
8		snidg	|- ( I e. U -> I e. { I } )
9	2 8	syl	|- ( ph -> I e. { I } )
10	9	olcd	|- ( ph -> ( I e. dom S \/ I e. { I } ) )
11		elun	|- ( I e. ( dom S u. { I } ) <-> ( I e. dom S \/ I e. { I } ) )
12	10 11	sylibr	|- ( ph -> I e. ( dom S u. { I } ) )
13	7 12	prssd	|- ( ph -> { ( Base ` ndx ) , I } C_ ( dom S u. { I } ) )
14		structex	|- ( S Struct X -> S e. _V )
15	1 14	syl	|- ( ph -> S e. _V )
16		setsdm	|- ( ( S e. _V /\ E e. W ) -> dom ( S sSet <. I , E >. ) = ( dom S u. { I } ) )
17	15 3 16	syl2anc	|- ( ph -> dom ( S sSet <. I , E >. ) = ( dom S u. { I } ) )
18	13 17	sseqtrrd	|- ( ph -> { ( Base ` ndx ) , I } C_ dom ( S sSet <. I , E >. ) )