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

Metamath Proof Explorer

Theorem funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998) (Proof shortened by SN, 19-Dec-2024)

Ref Expression
Assertion funmo ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 )

Proof

Step Hyp Ref Expression
1 dffun6 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
2 1 simplbi ⊢ ( Fun 𝐹 → Rel 𝐹 )
3 brrelex1 ⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝑦 ) → 𝐴 ∈ V )
4 3 ex ⊢ ( Rel 𝐹 → ( 𝐴 𝐹 𝑦 → 𝐴 ∈ V ) )
5 2 4 syl ⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝑦 → 𝐴 ∈ V ) )
6 5 ancrd ⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝑦 → ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ) )
7 6 alrimiv ⊢ ( Fun 𝐹 → ∀ 𝑦 ( 𝐴 𝐹 𝑦 → ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ) )
8 1 simprbi ⊢ ( Fun 𝐹 → ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 )
9 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
10 9 mobidv ⊢ ( 𝑥 = 𝐴 → ( ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∃* 𝑦 𝐴 𝐹 𝑦 ) )
11 10 spcgv ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
12 8 11 syl5com ⊢ ( Fun 𝐹 → ( 𝐴 ∈ V → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
13 moanimv ⊢ ( ∃* 𝑦 ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ↔ ( 𝐴 ∈ V → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
14 12 13 sylibr ⊢ ( Fun 𝐹 → ∃* 𝑦 ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) )
15 moim ⊢ ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 → ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ) → ( ∃* 𝑦 ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
16 7 14 15 sylc ⊢ ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 )