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	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 𝐵 } ) )