This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )