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 ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
Assertion funcsetcestrclem1 ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2 funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
5 opeq2 ⊢ ( 𝑥 = 𝑋 → ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ )
6 5 sneqd ⊢ ( 𝑥 = 𝑋 → { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )
7 6 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) ∧ 𝑥 = 𝑋 ) → { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝐶 )
9 snex ⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ∈ V
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ∈ V )
11 4 7 8 10 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )