Theorem 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	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 1o } ) )
Assertion	f1omo	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		f1omo.1	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 1o } ) )
2		1oex	⊢ 1o ∈ V
3		eqid	⊢ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = ( ( 𝐴 × { 1o } ) ‘ 𝑋 )
4	2 3	fvconst0ci	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o )
5		mo0	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = ∅ → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
6		df1o2	⊢ 1o = { ∅ }
7	6	eqeq2i	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o ↔ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = { ∅ } )
8		mosn	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = { ∅ } → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
9	7 8	sylbi	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
10	5 9	jaoi	⊢ ( ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
11	4 10	ax-mp	⊢ ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 )
12	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
13	12	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ) )
14	13	mobidv	⊢ ( 𝜑 → ( ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ) )
15	11 14	mpbiri	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )