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 ‘ 𝑝 ) )