Metamath Proof Explorer


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 >. ) )