# Metamath Proof Explorer

## Theorem fgreu

Description: Exactly one point of a function's graph has a given first element. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion fgreu ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to \exists !{p}\in {F}\phantom{\rule{.4em}{0ex}}{X}={1}^{st}\left({p}\right)$

### Proof

Step Hyp Ref Expression
1 funfvop ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to ⟨{X},{F}\left({X}\right)⟩\in {F}$
2 simplll ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to \mathrm{Fun}{F}$
3 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
4 2 3 syl ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to \mathrm{Rel}{F}$
5 simplr ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {p}\in {F}$
6 1st2nd ${⊢}\left(\mathrm{Rel}{F}\wedge {p}\in {F}\right)\to {p}=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
7 4 5 6 syl2anc ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {p}=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
8 simpr ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {X}={1}^{st}\left({p}\right)$
9 simpllr ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {X}\in \mathrm{dom}{F}$
10 8 opeq1d ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to ⟨{X},{2}^{nd}\left({p}\right)⟩=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
11 7 10 eqtr4d ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {p}=⟨{X},{2}^{nd}\left({p}\right)⟩$
12 11 5 eqeltrrd ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to ⟨{X},{2}^{nd}\left({p}\right)⟩\in {F}$
13 funopfvb ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to \left({F}\left({X}\right)={2}^{nd}\left({p}\right)↔⟨{X},{2}^{nd}\left({p}\right)⟩\in {F}\right)$
14 13 biimpar ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge ⟨{X},{2}^{nd}\left({p}\right)⟩\in {F}\right)\to {F}\left({X}\right)={2}^{nd}\left({p}\right)$
15 2 9 12 14 syl21anc ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {F}\left({X}\right)={2}^{nd}\left({p}\right)$
16 8 15 opeq12d ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to ⟨{X},{F}\left({X}\right)⟩=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
17 7 16 eqtr4d ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {X}={1}^{st}\left({p}\right)\right)\to {p}=⟨{X},{F}\left({X}\right)⟩$
18 simpr ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {p}=⟨{X},{F}\left({X}\right)⟩\right)\to {p}=⟨{X},{F}\left({X}\right)⟩$
19 18 fveq2d ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {p}=⟨{X},{F}\left({X}\right)⟩\right)\to {1}^{st}\left({p}\right)={1}^{st}\left(⟨{X},{F}\left({X}\right)⟩\right)$
20 fvex ${⊢}{F}\left({X}\right)\in \mathrm{V}$
21 op1stg ${⊢}\left({X}\in \mathrm{dom}{F}\wedge {F}\left({X}\right)\in \mathrm{V}\right)\to {1}^{st}\left(⟨{X},{F}\left({X}\right)⟩\right)={X}$
22 20 21 mpan2 ${⊢}{X}\in \mathrm{dom}{F}\to {1}^{st}\left(⟨{X},{F}\left({X}\right)⟩\right)={X}$
23 22 ad3antlr ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {p}=⟨{X},{F}\left({X}\right)⟩\right)\to {1}^{st}\left(⟨{X},{F}\left({X}\right)⟩\right)={X}$
24 19 23 eqtr2d ${⊢}\left(\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\wedge {p}=⟨{X},{F}\left({X}\right)⟩\right)\to {X}={1}^{st}\left({p}\right)$
25 17 24 impbida ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\wedge {p}\in {F}\right)\to \left({X}={1}^{st}\left({p}\right)↔{p}=⟨{X},{F}\left({X}\right)⟩\right)$
26 25 ralrimiva ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to \forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}=⟨{X},{F}\left({X}\right)⟩\right)$
27 eqeq2 ${⊢}{q}=⟨{X},{F}\left({X}\right)⟩\to \left({p}={q}↔{p}=⟨{X},{F}\left({X}\right)⟩\right)$
28 27 bibi2d ${⊢}{q}=⟨{X},{F}\left({X}\right)⟩\to \left(\left({X}={1}^{st}\left({p}\right)↔{p}={q}\right)↔\left({X}={1}^{st}\left({p}\right)↔{p}=⟨{X},{F}\left({X}\right)⟩\right)\right)$
29 28 ralbidv ${⊢}{q}=⟨{X},{F}\left({X}\right)⟩\to \left(\forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}={q}\right)↔\forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}=⟨{X},{F}\left({X}\right)⟩\right)\right)$
30 29 rspcev ${⊢}\left(⟨{X},{F}\left({X}\right)⟩\in {F}\wedge \forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}=⟨{X},{F}\left({X}\right)⟩\right)\right)\to \exists {q}\in {F}\phantom{\rule{.4em}{0ex}}\forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}={q}\right)$
31 1 26 30 syl2anc ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to \exists {q}\in {F}\phantom{\rule{.4em}{0ex}}\forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}={q}\right)$
32 reu6 ${⊢}\exists !{p}\in {F}\phantom{\rule{.4em}{0ex}}{X}={1}^{st}\left({p}\right)↔\exists {q}\in {F}\phantom{\rule{.4em}{0ex}}\forall {p}\in {F}\phantom{\rule{.4em}{0ex}}\left({X}={1}^{st}\left({p}\right)↔{p}={q}\right)$
33 31 32 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to \exists !{p}\in {F}\phantom{\rule{.4em}{0ex}}{X}={1}^{st}\left({p}\right)$