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 ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 )