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	$$⊢\phi \to U=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\right)$$
	prdsbaslem.1	$$⊢A=E\left(U\right)$$
	prdsbaslem.2	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	prdsbaslem.3	$$⊢\phi \to T\in V$$
	prdsbaslem.4	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),T⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\right)$$
Assertion	prdsbaslem	$$⊢\phi \to A=T$$

Proof

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