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

Metamath Proof Explorer

Theorem 2strop

Description: The other slot of a constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020)

		Ref	Expression
	Hypotheses	2str.g	$⊢ G = \{⟨{Base}_{ndx}, B⟩, ⟨N, \underset{˙}{+}⟩\}$
		2str.b	$⊢ {Base}_{ndx} < N$
		2str.n	$⊢ N \in ℕ$
		2str.e	$⊢ E = Slot N$
	Assertion	2strop	$⊢ \underset{˙}{+} \in V \to \underset{˙}{+} = E (G)$

Proof

Step	Hyp	Ref	Expression
1		2str.g	$⊢ G = \{⟨{Base}_{ndx}, B⟩, ⟨N, \underset{˙}{+}⟩\}$
2		2str.b	$⊢ {Base}_{ndx} < N$
3		2str.n	$⊢ N \in ℕ$
4		2str.e	$⊢ E = Slot N$
5	1 2 3	2strstr	$⊢ G Struct ⟨{Base}_{ndx}, N⟩$
6	4 3	ndxid	$⊢ E = Slot E (ndx)$
7		snsspr2	$⊢ \{⟨N, \underset{˙}{+}⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨N, \underset{˙}{+}⟩\}$
8	4 3	ndxarg	$⊢ E (ndx) = N$
9	8	opeq1i	$⊢ ⟨E (ndx), \underset{˙}{+}⟩ = ⟨N, \underset{˙}{+}⟩$
10	9	sneqi	$⊢ \{⟨E (ndx), \underset{˙}{+}⟩\} = \{⟨N, \underset{˙}{+}⟩\}$
11	7 10 1	3sstr4i	$⊢ \{⟨E (ndx), \underset{˙}{+}⟩\} \subseteq G$
12	5 6 11	strfv	$⊢ \underset{˙}{+} \in V \to \underset{˙}{+} = E (G)$