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

Metamath Proof Explorer

Theorem fvconst0ci

Description: A constant function's value is either the constant or the empty set. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024)

		Ref	Expression
	Hypotheses	fvconst0ci.1	⊢ 𝐵 ∈ V
		fvconst0ci.2	⊢ 𝑌 = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 )
	Assertion	fvconst0ci	⊢ ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvconst0ci.1	⊢ 𝐵 ∈ V
2		fvconst0ci.2	⊢ 𝑌 = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 )
3		dmxpss	⊢ dom ( 𝐴 × { 𝐵 } ) ⊆ 𝐴
4	3	sseli	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑋 ∈ 𝐴 )
5	1	fvconst2	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 )
6	4 5	syl	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 )
7	2 6	eqtrid	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑌 = 𝐵 )
8	7	olcd	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 ) )
9		ndmfv	⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = ∅ )
10	2 9	eqtrid	⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑌 = ∅ )
11	10	orcd	⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 ) )
12	8 11	pm2.61i	⊢ ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 )