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	$⊢ B \in V$
	Assertion	fvconstdomi	$⊢ (A \times \{B\}) (X) ≼ B$

Proof

Step	Hyp	Ref	Expression
1		fvconstdomi.1	$⊢ B \in V$
2		dmxpss	$⊢ dom (A \times \{B\}) \subseteq A$
3	2	sseli	$⊢ X \in dom (A \times \{B\}) \to X \in A$
4	1	fvconst2	$⊢ X \in A \to (A \times \{B\}) (X) = B$
5	3 4	syl	$⊢ X \in dom (A \times \{B\}) \to (A \times \{B\}) (X) = B$
6		domrefg	$⊢ B \in V \to B ≼ B$
7	1 6	ax-mp	$⊢ B ≼ B$
8	5 7	eqbrtrdi	$⊢ X \in dom (A \times \{B\}) \to (A \times \{B\}) (X) ≼ B$
9		ndmfv	$⊢ \neg X \in dom (A \times \{B\}) \to (A \times \{B\}) (X) = \emptyset$
10	1	0dom	$⊢ \emptyset ≼ B$
11	9 10	eqbrtrdi	$⊢ \neg X \in dom (A \times \{B\}) \to (A \times \{B\}) (X) ≼ B$
12	8 11	pm2.61i	$⊢ (A \times \{B\}) (X) ≼ B$