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 ) , 𝑋 ⟩ } )