Theorem f1omoALT

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.) Use f1omo without assuming ax-un . (Contributed by Zhi Wang, 18-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	f1omoALT.1	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 1o } ) )
Assertion	f1omoALT	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		f1omoALT.1	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 1o } ) )
2	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
3		1oex	⊢ 1o ∈ V
4	3	fvconstdomi	⊢ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ≼ 1o
5	2 4	eqbrtrdi	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≼ 1o )
6		modom2	⊢ ( ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) ≼ 1o )
7	5 6	sylibr	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )