This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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