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

Metamath Proof Explorer

Theorem prdsbaslem

Description: Lemma for prdsbas and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 12-Jul-2024)

		Ref	Expression
	Hypotheses	prdsbaslem.u	$⊢ φ \to U = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, L⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
		prdsbaslem.1	$⊢ A = E (U)$
		prdsbaslem.2	$⊢ E = Slot E (ndx)$
		prdsbaslem.3	$⊢ φ \to T \in V$
		prdsbaslem.4	$⊢ \{⟨E (ndx), T⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, L⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
	Assertion	prdsbaslem	$⊢ φ \to A = T$

Proof

Step	Hyp	Ref	Expression
1		prdsbaslem.u	$⊢ φ \to U = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, L⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
2		prdsbaslem.1	$⊢ A = E (U)$
3		prdsbaslem.2	$⊢ E = Slot E (ndx)$
4		prdsbaslem.3	$⊢ φ \to T \in V$
5		prdsbaslem.4	$⊢ \{⟨E (ndx), T⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, L⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
6		prdsvalstr	$⊢ ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, L⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})) Struct ⟨1, 15⟩$
7	1 6 3 5 4 2	strfv3	$⊢ φ \to A = T$