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

Metamath Proof Explorer

Theorem fmptff

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses fmptff.1 ⊢ Ⅎ 𝑥 𝐴
fmptff.2 ⊢ Ⅎ 𝑥 𝐵
fmptff.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion fmptff ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 fmptff.1 ⊢ Ⅎ 𝑥 𝐴
2 fmptff.2 ⊢ Ⅎ 𝑥 𝐵
3 fmptff.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
4 nfcv ⊢ Ⅎ 𝑦 𝐴
5 nfv ⊢ Ⅎ 𝑦 𝐶 ∈ 𝐵
6 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
7 6 2 nfel ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵
8 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
9 8 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∈ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) )
10 1 4 5 7 9 cbvralfw ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 )
11 nfcv ⊢ Ⅎ 𝑦 𝐶
12 1 4 11 6 8 cbvmptf ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
13 3 12 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
14 13 fmpt ⊢ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
15 10 14 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )