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 ⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
basprssdmsets.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
basprssdmsets.w ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
basprssdmsets.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
Assertion basprssdmsets ( 𝜑 → { ( Base ‘ ndx ) , 𝐼 } ⊆ dom ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )

Proof

Step Hyp Ref Expression
1 basprssdmsets.s ⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
2 basprssdmsets.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
3 basprssdmsets.w ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4 basprssdmsets.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
5 4 orcd ⊢ ( 𝜑 → ( ( Base ‘ ndx ) ∈ dom 𝑆 ∨ ( Base ‘ ndx ) ∈ { 𝐼 } ) )
6 elun ⊢ ( ( Base ‘ ndx ) ∈ ( dom 𝑆 ∪ { 𝐼 } ) ↔ ( ( Base ‘ ndx ) ∈ dom 𝑆 ∨ ( Base ‘ ndx ) ∈ { 𝐼 } ) )
7 5 6 sylibr ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ ( dom 𝑆 ∪ { 𝐼 } ) )
8 snidg ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ { 𝐼 } )
9 2 8 syl ⊢ ( 𝜑 → 𝐼 ∈ { 𝐼 } )
10 9 olcd ⊢ ( 𝜑 → ( 𝐼 ∈ dom 𝑆 ∨ 𝐼 ∈ { 𝐼 } ) )
11 elun ⊢ ( 𝐼 ∈ ( dom 𝑆 ∪ { 𝐼 } ) ↔ ( 𝐼 ∈ dom 𝑆 ∨ 𝐼 ∈ { 𝐼 } ) )
12 10 11 sylibr ⊢ ( 𝜑 → 𝐼 ∈ ( dom 𝑆 ∪ { 𝐼 } ) )
13 7 12 prssd ⊢ ( 𝜑 → { ( Base ‘ ndx ) , 𝐼 } ⊆ ( dom 𝑆 ∪ { 𝐼 } ) )
14 structex ⊢ ( 𝑆 Struct 𝑋 → 𝑆 ∈ V )
15 1 14 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
16 setsdm ⊢ ( ( 𝑆 ∈ V ∧ 𝐸 ∈ 𝑊 ) → dom ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( dom 𝑆 ∪ { 𝐼 } ) )
17 15 3 16 syl2anc ⊢ ( 𝜑 → dom ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( dom 𝑆 ∪ { 𝐼 } ) )
18 13 17 sseqtrrd ⊢ ( 𝜑 → { ( Base ‘ ndx ) , 𝐼 } ⊆ dom ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )