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

Metamath Proof Explorer

Theorem funcestrcsetclem1

Description: Lemma 1 for funcestrcsetc . (Contributed by AV, 22-Mar-2020)

Ref Expression
Hypotheses funcestrcsetc.e ⊢ E = ExtStrCat ⁡ U
funcestrcsetc.s ⊢ S = SetCat ⁡ U
funcestrcsetc.b ⊢ B = Base E
funcestrcsetc.c ⊢ C = Base S
funcestrcsetc.u ⊢ φ → U ∈ WUni
funcestrcsetc.f ⊢ φ → F = x ∈ B ⟼ Base x
Assertion funcestrcsetclem1 ⊢ φ ∧ X ∈ B → F ⁡ X = Base X

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ⊢ E = ExtStrCat ⁡ U
2 funcestrcsetc.s ⊢ S = SetCat ⁡ U
3 funcestrcsetc.b ⊢ B = Base E
4 funcestrcsetc.c ⊢ C = Base S
5 funcestrcsetc.u ⊢ φ → U ∈ WUni
6 funcestrcsetc.f ⊢ φ → F = x ∈ B ⟼ Base x
7 6 adantr ⊢ φ ∧ X ∈ B → F = x ∈ B ⟼ Base x
8 fveq2 ⊢ x = X → Base x = Base X
9 8 adantl ⊢ φ ∧ X ∈ B ∧ x = X → Base x = Base X
10 simpr ⊢ φ ∧ X ∈ B → X ∈ B
11 fvexd ⊢ φ ∧ X ∈ B → Base X ∈ V
12 7 9 10 11 fvmptd ⊢ φ ∧ X ∈ B → F ⁡ X = Base X