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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) ≼ 𝐵