Theorem fvconstdomi

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

	Ref	Expression
Hypothesis	fvconstdomi.1	⊢ 𝐵 ∈ V
Assertion	fvconstdomi	⊢ ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) ≼ 𝐵

Proof

Step	Hyp	Ref	Expression
1		fvconstdomi.1	⊢ 𝐵 ∈ V
2		dmxpss	⊢ dom ( 𝐴 × { 𝐵 } ) ⊆ 𝐴
3	2	sseli	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑋 ∈ 𝐴 )
4	1	fvconst2	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 )
5	3 4	syl	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 )
6		domrefg	⊢ ( 𝐵 ∈ V → 𝐵 ≼ 𝐵 )
7	1 6	ax-mp	⊢ 𝐵 ≼ 𝐵
8	5 7	eqbrtrdi	⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) ≼ 𝐵 )
9		ndmfv	⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = ∅ )
10	1	0dom	⊢ ∅ ≼ 𝐵
11	9 10	eqbrtrdi	⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) ≼ 𝐵 )
12	8 11	pm2.61i	⊢ ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) ≼ 𝐵