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

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 ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ∃! 𝑝 ∈ 𝐹 𝑋 = ( 1st ‘ 𝑝 ) )

Proof

Step Hyp Ref Expression
1 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 )
2 simplll ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → Fun 𝐹 )
3 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
4 2 3 syl ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → Rel 𝐹 )
5 simplr ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → 𝑝 ∈ 𝐹 )
6 1st2nd ⊢ ( ( Rel 𝐹 ∧ 𝑝 ∈ 𝐹 ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
7 4 5 6 syl2anc ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
8 simpr ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → 𝑋 = ( 1st ‘ 𝑝 ) )
9 simpllr ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → 𝑋 ∈ dom 𝐹 )
10 8 opeq1d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → ⟨ 𝑋 , ( 2nd ‘ 𝑝 ) ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
11 7 10 eqtr4d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → 𝑝 = ⟨ 𝑋 , ( 2nd ‘ 𝑝 ) ⟩ )
12 11 5 eqeltrrd ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → ⟨ 𝑋 , ( 2nd ‘ 𝑝 ) ⟩ ∈ 𝐹 )
13 funopfvb ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 2nd ‘ 𝑝 ) ↔ ⟨ 𝑋 , ( 2nd ‘ 𝑝 ) ⟩ ∈ 𝐹 ) )
14 13 biimpar ⊢ ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ ⟨ 𝑋 , ( 2nd ‘ 𝑝 ) ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 2nd ‘ 𝑝 ) )
15 2 9 12 14 syl21anc ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑋 ) = ( 2nd ‘ 𝑝 ) )
16 8 15 opeq12d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
17 7 16 eqtr4d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑋 = ( 1st ‘ 𝑝 ) ) → 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ )
18 simpr ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) → 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ )
19 18 fveq2d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) → ( 1st ‘ 𝑝 ) = ( 1st ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) )
20 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
21 op1stg ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ) → ( 1st ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) = 𝑋 )
22 20 21 mpan2 ⊢ ( 𝑋 ∈ dom 𝐹 → ( 1st ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) = 𝑋 )
23 22 ad3antlr ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) → ( 1st ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) = 𝑋 )
24 19 23 eqtr2d ⊢ ( ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) ∧ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) → 𝑋 = ( 1st ‘ 𝑝 ) )
25 17 24 impbida ⊢ ( ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) ∧ 𝑝 ∈ 𝐹 ) → ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) )
26 25 ralrimiva ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) )
27 eqeq2 ⊢ ( 𝑞 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ → ( 𝑝 = 𝑞 ↔ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) )
28 27 bibi2d ⊢ ( 𝑞 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ → ( ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = 𝑞 ) ↔ ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) ) )
29 28 ralbidv ⊢ ( 𝑞 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ → ( ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = 𝑞 ) ↔ ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) ) )
30 29 rspcev ⊢ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ∧ ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) ) → ∃ 𝑞 ∈ 𝐹 ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = 𝑞 ) )
31 1 26 30 syl2anc ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ∃ 𝑞 ∈ 𝐹 ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = 𝑞 ) )
32 reu6 ⊢ ( ∃! 𝑝 ∈ 𝐹 𝑋 = ( 1st ‘ 𝑝 ) ↔ ∃ 𝑞 ∈ 𝐹 ∀ 𝑝 ∈ 𝐹 ( 𝑋 = ( 1st ‘ 𝑝 ) ↔ 𝑝 = 𝑞 ) )
33 31 32 sylibr ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ∃! 𝑝 ∈ 𝐹 𝑋 = ( 1st ‘ 𝑝 ) )