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)

	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		el1o	⊢ ( 𝑦 ∈ 1o ↔ 𝑦 = ∅ )
7		el1o	⊢ ( 𝑥 ∈ 1o ↔ 𝑥 = ∅ )
8		eqtr3	⊢ ( ( 𝑦 = ∅ ∧ 𝑥 = ∅ ) → 𝑦 = 𝑥 )
9	6 7 8	syl2anb	⊢ ( ( 𝑦 ∈ 1o ∧ 𝑥 ∈ 1o ) → 𝑦 = 𝑥 )
10	9	gen2	⊢ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 1o ∧ 𝑥 ∈ 1o ) → 𝑦 = 𝑥 )
11		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 1o ↔ 𝑥 ∈ 1o ) )
12	11	mo4	⊢ ( ∃* 𝑦 𝑦 ∈ 1o ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 1o ∧ 𝑥 ∈ 1o ) → 𝑦 = 𝑥 ) )
13	10 12	mpbir	⊢ ∃* 𝑦 𝑦 ∈ 1o
14		eleq2w2	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o → ( 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ↔ 𝑦 ∈ 1o ) )
15	14	mobidv	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o → ( ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ↔ ∃* 𝑦 𝑦 ∈ 1o ) )
16	13 15	mpbiri	⊢ ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
17	5 16	jaoi	⊢ ( ( ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) = 1o ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
18	4 17	ax-mp	⊢ ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 )
19	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) )
20	19	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ) )
21	20	mobidv	⊢ ( 𝜑 → ( ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1o } ) ‘ 𝑋 ) ) )
22	18 21	mpbiri	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )