fconst7v

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022) Removed hyphotheses as suggested by SN (Revised by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	fconst7v.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	fconst7v.e	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
Assertion	fconst7v	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		fconst7v.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		fconst7v.e	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
3		0xp	⊢ ( ∅ × { 𝐵 } ) = ∅
4	3	a1i	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ∅ × { 𝐵 } ) = ∅ )
5		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
6	5	xpeq1d	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝐴 × { 𝐵 } ) = ( ∅ × { 𝐵 } ) )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐹 Fn 𝐴 )
8		fneq2	⊢ ( 𝐴 = ∅ → ( 𝐹 Fn 𝐴 ↔ 𝐹 Fn ∅ ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝐹 Fn 𝐴 ↔ 𝐹 Fn ∅ ) )
10	7 9	mpbid	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐹 Fn ∅ )
11		fn0	⊢ ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )
12	10 11	sylib	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐹 = ∅ )
13	4 6 12	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐹 = ( 𝐴 × { 𝐵 } ) )
14		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
15	2 14	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
16		snidg	⊢ ( 𝐵 ∈ V → 𝐵 ∈ { 𝐵 } )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ { 𝐵 } )
18	2 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } )
19	18	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } )
20		nfcv	⊢ Ⅎ 𝑥 𝐴
21		nfcv	⊢ Ⅎ 𝑥 { 𝐵 }
22		nfcv	⊢ Ⅎ 𝑥 𝐹
23	20 21 22	ffnfvf	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ) )
24	1 19 23	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ { 𝐵 } )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐹 : 𝐴 ⟶ { 𝐵 } )
26		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
27	15	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
28	26 27	n0limd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ V )
29		fconst2g	⊢ ( 𝐵 ∈ V → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
30	28 29	syl	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
31	25 30	mpbid	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐹 = ( 𝐴 × { 𝐵 } ) )
32		exmidne	⊢ ( 𝐴 = ∅ ∨ 𝐴 ≠ ∅ )
33	32	a1i	⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ 𝐴 ≠ ∅ ) )
34	13 31 33	mpjaodan	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 𝐵 } ) )

Metamath Proof Explorer

Theorem fconst7v

Proof