f1omo

Description: There is at most one element in the function value of a constant function whose output is 1o . (An artifact of our function value definition.) Proof could be significantly shortened by fvconstdomi assuming ax-un (see f1omoALT ). (Contributed by Zhi Wang, 19-Sep-2024) (Proof shortened by SN, 24-Nov-2025)

		Ref	Expression
	Hypothesis	f1omo.1	$⊢ φ \to F = A \times \{1_{𝑜}\}$
	Assertion	f1omo	$⊢ φ \to \exists^{*} y y \in F (X)$

Proof

Step	Hyp	Ref	Expression
1		f1omo.1	$⊢ φ \to F = A \times \{1_{𝑜}\}$
2		1oex	$⊢ 1_{𝑜} \in V$
3		eqid	$⊢ (A \times \{1_{𝑜}\}) (X) = (A \times \{1_{𝑜}\}) (X)$
4	2 3	fvconst0ci	$⊢ ((A \times \{1_{𝑜}\}) (X) = \emptyset \lor (A \times \{1_{𝑜}\}) (X) = 1_{𝑜})$
5		mo0	$⊢ (A \times \{1_{𝑜}\}) (X) = \emptyset \to \exists^{*} y y \in (A \times \{1_{𝑜}\}) (X)$
6		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
7	6	eqeq2i	$⊢ (A \times \{1_{𝑜}\}) (X) = 1_{𝑜} \leftrightarrow (A \times \{1_{𝑜}\}) (X) = \{\emptyset\}$
8		mosn	$⊢ (A \times \{1_{𝑜}\}) (X) = \{\emptyset\} \to \exists^{*} y y \in (A \times \{1_{𝑜}\}) (X)$
9	7 8	sylbi	$⊢ (A \times \{1_{𝑜}\}) (X) = 1_{𝑜} \to \exists^{*} y y \in (A \times \{1_{𝑜}\}) (X)$
10	5 9	jaoi	$⊢ ((A \times \{1_{𝑜}\}) (X) = \emptyset \lor (A \times \{1_{𝑜}\}) (X) = 1_{𝑜}) \to \exists^{*} y y \in (A \times \{1_{𝑜}\}) (X)$
11	4 10	ax-mp	$⊢ \exists^{*} y y \in (A \times \{1_{𝑜}\}) (X)$
12	1	fveq1d	$⊢ φ \to F (X) = (A \times \{1_{𝑜}\}) (X)$
13	12	eleq2d	$⊢ φ \to (y \in F (X) \leftrightarrow y \in (A \times \{1_{𝑜}\}) (X))$
14	13	mobidv	$⊢ φ \to (\exists^{} y y \in F (X) \leftrightarrow \exists^{} y y \in (A \times \{1_{𝑜}\}) (X))$
15	11 14	mpbiri	$⊢ φ \to \exists^{*} y y \in F (X)$

Metamath Proof Explorer

Theorem f1omo

Proof