Metamath Proof Explorer

Theorem estrreslem1

Description: Lemma 1 for estrres . (Contributed by AV, 14-Mar-2020) (Proof shortened by AV, 28-Oct-2024)

		Ref	Expression
	Hypotheses	estrres.c	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
		estrres.b	$⊢ φ \to B \in V$
	Assertion	estrreslem1	$⊢ φ \to B = {Base}_{C}$

Proof

Step	Hyp	Ref	Expression
1		estrres.c	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
2		estrres.b	$⊢ φ \to B \in V$
3	1	fveq2d	$⊢ φ \to {Base}_{C} = {Base}_{\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}}$
4		baseid	$⊢ Base = Slot {Base}_{ndx}$
5		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
6	5	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
7	4 6	strfvnd	$⊢ φ \to {Base}_{\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} ({Base}_{ndx})$
8		fvexd	$⊢ φ \to {Base}_{ndx} \in V$
9		slotsbhcdif	$⊢ ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx) \land Hom (ndx) \neq comp (ndx))$
10		3simpa	$⊢ ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx) \land Hom (ndx) \neq comp (ndx)) \to ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx))$
11	9 10	mp1i	$⊢ φ \to ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx))$
12		fvtp1g	$⊢ (({Base}_{ndx} \in V \land B \in V) \land ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx))) \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} ({Base}_{ndx}) = B$
13	8 2 11 12	syl21anc	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} ({Base}_{ndx}) = B$
14	3 7 13	3eqtrrd	$⊢ φ \to B = {Base}_{C}$