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 ⟨ 𝐼 , 𝐸 ⟩ ) )