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	$⊢ φ \to S Struct X$
	basprssdmsets.i	$⊢ φ \to I \in U$
	basprssdmsets.w	$⊢ φ \to E \in W$
	basprssdmsets.b	$⊢ φ \to {Base}_{ndx} \in dom S$
Assertion	basprssdmsets	$⊢ φ \to \{{Base}_{ndx}, I\} \subseteq dom (S sSet ⟨I, E⟩)$

Proof

Step	Hyp	Ref	Expression
1		basprssdmsets.s	$⊢ φ \to S Struct X$
2		basprssdmsets.i	$⊢ φ \to I \in U$
3		basprssdmsets.w	$⊢ φ \to E \in W$
4		basprssdmsets.b	$⊢ φ \to {Base}_{ndx} \in dom S$
5	4	orcd	$⊢ φ \to ({Base}_{ndx} \in dom S \lor {Base}_{ndx} \in \{I\})$
6		elun	$⊢ {Base}_{ndx} \in (dom S \cup \{I\}) \leftrightarrow ({Base}_{ndx} \in dom S \lor {Base}_{ndx} \in \{I\})$
7	5 6	sylibr	$⊢ φ \to {Base}_{ndx} \in (dom S \cup \{I\})$
8		snidg	$⊢ I \in U \to I \in \{I\}$
9	2 8	syl	$⊢ φ \to I \in \{I\}$
10	9	olcd	$⊢ φ \to (I \in dom S \lor I \in \{I\})$
11		elun	$⊢ I \in (dom S \cup \{I\}) \leftrightarrow (I \in dom S \lor I \in \{I\})$
12	10 11	sylibr	$⊢ φ \to I \in (dom S \cup \{I\})$
13	7 12	prssd	$⊢ φ \to \{{Base}_{ndx}, I\} \subseteq dom S \cup \{I\}$
14		structex	$⊢ S Struct X \to S \in V$
15	1 14	syl	$⊢ φ \to S \in V$
16		setsdm	$⊢ (S \in V \land E \in W) \to dom (S sSet ⟨I, E⟩) = dom S \cup \{I\}$
17	15 3 16	syl2anc	$⊢ φ \to dom (S sSet ⟨I, E⟩) = dom S \cup \{I\}$
18	13 17	sseqtrrd	$⊢ φ \to \{{Base}_{ndx}, I\} \subseteq dom (S sSet ⟨I, E⟩)$

Metamath Proof Explorer

Theorem basprssdmsets

Proof