nvocnv

Description: The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019)

		Ref	Expression
	Assertion	nvocnv	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to F^{-1} = F$

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to y = F (z)$
2		simpll	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to F : A ⟶ A$
3		simprl	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to z \in A$
4	2 3	ffvelrnd	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to F (z) \in A$
5	1 4	eqeltrd	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to y \in A$
6	1	fveq2d	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to F (y) = F (F (z))$
7		2fveq3	$⊢ x = z \to F (F (x)) = F (F (z))$
8		id	$⊢ x = z \to x = z$
9	7 8	eqeq12d	$⊢ x = z \to (F (F (x)) = x \leftrightarrow F (F (z)) = z)$
10		simplr	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to \forall x \in A F (F (x)) = x$
11	9 10 3	rspcdva	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to F (F (z)) = z$
12	6 11	eqtr2d	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to z = F (y)$
13	5 12	jca	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (z \in A \land y = F (z))) \to (y \in A \land z = F (y))$
14		simprr	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to z = F (y)$
15		simpll	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to F : A ⟶ A$
16		simprl	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to y \in A$
17	15 16	ffvelrnd	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to F (y) \in A$
18	14 17	eqeltrd	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to z \in A$
19	14	fveq2d	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to F (z) = F (F (y))$
20		2fveq3	$⊢ x = y \to F (F (x)) = F (F (y))$
21		id	$⊢ x = y \to x = y$
22	20 21	eqeq12d	$⊢ x = y \to (F (F (x)) = x \leftrightarrow F (F (y)) = y)$
23		simplr	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to \forall x \in A F (F (x)) = x$
24	22 23 16	rspcdva	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to F (F (y)) = y$
25	19 24	eqtr2d	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to y = F (z)$
26	18 25	jca	$⊢ ((F : A ⟶ A \land \forall x \in A F (F (x)) = x) \land (y \in A \land z = F (y))) \to (z \in A \land y = F (z))$
27	13 26	impbida	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to ((z \in A \land y = F (z)) \leftrightarrow (y \in A \land z = F (y)))$
28	27	mptcnv	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to {(z \in A ⟼ F (z))}^{-1} = (y \in A ⟼ F (y))$
29		ffn	$⊢ F : A ⟶ A \to F Fn A$
30		dffn5	$⊢ F Fn A \leftrightarrow F = (z \in A ⟼ F (z))$
31	30	biimpi	$⊢ F Fn A \to F = (z \in A ⟼ F (z))$
32	31	adantr	$⊢ (F Fn A \land \forall x \in A F (F (x)) = x) \to F = (z \in A ⟼ F (z))$
33	29 32	sylan	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to F = (z \in A ⟼ F (z))$
34	33	cnveqd	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to F^{-1} = {(z \in A ⟼ F (z))}^{-1}$
35		dffn5	$⊢ F Fn A \leftrightarrow F = (y \in A ⟼ F (y))$
36	35	biimpi	$⊢ F Fn A \to F = (y \in A ⟼ F (y))$
37	36	adantr	$⊢ (F Fn A \land \forall x \in A F (F (x)) = x) \to F = (y \in A ⟼ F (y))$
38	29 37	sylan	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to F = (y \in A ⟼ F (y))$
39	28 34 38	3eqtr4d	$⊢ (F : A ⟶ A \land \forall x \in A F (F (x)) = x) \to F^{-1} = F$

Metamath Proof Explorer

Theorem nvocnv

Proof