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

Metamath Proof Explorer

Theorem funcsetcestrclem1

Description: Lemma 1 for funcsetcestrc . (Contributed by AV, 27-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ S = SetCat ⁡ U
funcsetcestrc.c ⊢ C = Base S
funcsetcestrc.f ⊢ φ → F = x ∈ C ⟼ Base ndx x
Assertion funcsetcestrclem1 ⊢ φ ∧ X ∈ C → F ⁡ X = Base ndx X

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ S = SetCat ⁡ U
2 funcsetcestrc.c ⊢ C = Base S
3 funcsetcestrc.f ⊢ φ → F = x ∈ C ⟼ Base ndx x
4 3 adantr ⊢ φ ∧ X ∈ C → F = x ∈ C ⟼ Base ndx x
5 opeq2 ⊢ x = X → Base ndx x = Base ndx X
6 5 sneqd ⊢ x = X → Base ndx x = Base ndx X
7 6 adantl ⊢ φ ∧ X ∈ C ∧ x = X → Base ndx x = Base ndx X
8 simpr ⊢ φ ∧ X ∈ C → X ∈ C
9 snex ⊢ Base ndx X ∈ V
10 9 a1i ⊢ φ ∧ X ∈ C → Base ndx X ∈ V
11 4 7 8 10 fvmptd ⊢ φ ∧ X ∈ C → F ⁡ X = Base ndx X