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

Metamath Proof Explorer

Theorem fconst7

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses fconst7.p ⊢ Ⅎ 𝑥 𝜑
fconst7.x ⊢ Ⅎ 𝑥 𝐹
fconst7.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fconst7.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
fconst7.e ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
Assertion fconst7 ( 𝜑 → 𝐹 = ( 𝐴 × { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 fconst7.p ⊢ Ⅎ 𝑥 𝜑
2 fconst7.x ⊢ Ⅎ 𝑥 𝐹
3 fconst7.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
4 fconst7.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
5 fconst7.e ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
6 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
7 5 6 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
8 snidg ⊢ ( 𝐵 ∈ V → 𝐵 ∈ { 𝐵 } )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ { 𝐵 } )
10 5 9 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } )
11 1 10 ralrimia ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } )
12 nfcv ⊢ Ⅎ 𝑥 𝐴
13 nfcv ⊢ Ⅎ 𝑥 { 𝐵 }
14 12 13 2 ffnfvf ⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ) )
15 3 11 14 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ { 𝐵 } )
16 fconst2g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
17 4 16 syl ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
18 15 17 mpbid ⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 𝐵 } ) )