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