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	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
	estrres.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion	estrreslem1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		estrres.c	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
2		estrres.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3	1	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ) )
4		baseid	⊢ Base = Slot ( Base ‘ ndx )
5		tpex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
6	5	a1i	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V )
7	4 6	strfvnd	⊢ ( 𝜑 → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) )
8		fvexd	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ V )
9		slotsbhcdif	⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
10		3simpa	⊢ ( ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ) → ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ) )
11	9 10	mp1i	⊢ ( 𝜑 → ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ) )
12		fvtp1g	⊢ ( ( ( ( Base ‘ ndx ) ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = 𝐵 )
13	8 2 11 12	syl21anc	⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = 𝐵 )
14	3 7 13	3eqtrrd	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )