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 F \land X \in dom F) \to \exists! p \in F X = 1^{st} (p)$

Proof

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

Metamath Proof Explorer

Theorem fgreu

Proof