f1eqcocnv

Description: Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015) (Proof shortened by Wolf Lammen, 29-May-2024)

		Ref	Expression
	Assertion	f1eqcocnv	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (F = G \leftrightarrow F^{-1} \circ G = {I ↾}_{A})$

Proof

Step	Hyp	Ref	Expression
1		f1cocnv1	$⊢ F : A \underset{1-1}{⟶} B \to F^{-1} \circ F = {I ↾}_{A}$
2		coeq2	$⊢ F = G \to F^{-1} \circ F = F^{-1} \circ G$
3	2	eqeq1d	$⊢ F = G \to (F^{-1} \circ F = {I ↾}_{A} \leftrightarrow F^{-1} \circ G = {I ↾}_{A})$
4	1 3	syl5ibcom	$⊢ F : A \underset{1-1}{⟶} B \to (F = G \to F^{-1} \circ G = {I ↾}_{A})$
5	4	adantr	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (F = G \to F^{-1} \circ G = {I ↾}_{A})$
6		f1fn	$⊢ G : A \underset{1-1}{⟶} B \to G Fn A$
7	6	adantl	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to G Fn A$
8	7	adantr	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \to G Fn A$
9		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
10	9	adantr	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to F Fn A$
11	10	adantr	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \to F Fn A$
12		equid	$⊢ x = x$
13		resieq	$⊢ (x \in A \land x \in A) \to (x ({I ↾}_{A}) x \leftrightarrow x = x)$
14	12 13	mpbiri	$⊢ (x \in A \land x \in A) \to x ({I ↾}_{A}) x$
15	14	anidms	$⊢ x \in A \to x ({I ↾}_{A}) x$
16	15	adantl	$⊢ (((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \land x \in A) \to x ({I ↾}_{A}) x$
17		breq	$⊢ F^{-1} \circ G = {I ↾}_{A} \to (x (F^{-1} \circ G) x \leftrightarrow x ({I ↾}_{A}) x)$
18	17	ad2antlr	$⊢ (((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \land x \in A) \to (x (F^{-1} \circ G) x \leftrightarrow x ({I ↾}_{A}) x)$
19	16 18	mpbird	$⊢ (((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \land x \in A) \to x (F^{-1} \circ G) x$
20		fnfun	$⊢ G Fn A \to Fun G$
21	7 20	syl	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to Fun G$
22	7	fndmd	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to dom G = A$
23	22	eleq2d	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (x \in dom G \leftrightarrow x \in A)$
24	23	biimpar	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to x \in dom G$
25		funopfvb	$⊢ (Fun G \land x \in dom G) \to (G (x) = y \leftrightarrow ⟨x, y⟩ \in G)$
26	21 24 25	syl2an2r	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (G (x) = y \leftrightarrow ⟨x, y⟩ \in G)$
27	26	bicomd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (⟨x, y⟩ \in G \leftrightarrow G (x) = y)$
28		df-br	$⊢ x G y \leftrightarrow ⟨x, y⟩ \in G$
29		eqcom	$⊢ y = G (x) \leftrightarrow G (x) = y$
30	27 28 29	3bitr4g	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (x G y \leftrightarrow y = G (x))$
31	30	biimpd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (x G y \to y = G (x))$
32		df-br	$⊢ x F y \leftrightarrow ⟨x, y⟩ \in F$
33		fnfun	$⊢ F Fn A \to Fun F$
34	10 33	syl	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to Fun F$
35	10	fndmd	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to dom F = A$
36	35	eleq2d	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (x \in dom F \leftrightarrow x \in A)$
37	36	biimpar	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to x \in dom F$
38		funopfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow ⟨x, y⟩ \in F)$
39	34 37 38	syl2an2r	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (F (x) = y \leftrightarrow ⟨x, y⟩ \in F)$
40	32 39	bitr4id	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (x F y \leftrightarrow F (x) = y)$
41		vex	$⊢ y \in V$
42		vex	$⊢ x \in V$
43	41 42	brcnv	$⊢ y F^{-1} x \leftrightarrow x F y$
44		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
45	40 43 44	3bitr4g	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (y F^{-1} x \leftrightarrow y = F (x))$
46	45	biimpd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (y F^{-1} x \to y = F (x))$
47	31 46	anim12d	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to ((x G y \land y F^{-1} x) \to (y = G (x) \land y = F (x)))$
48	47	eximdv	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (\exists y (x G y \land y F^{-1} x) \to \exists y (y = G (x) \land y = F (x)))$
49	42 42	brco	$⊢ x (F^{-1} \circ G) x \leftrightarrow \exists y (x G y \land y F^{-1} x)$
50		fvex	$⊢ G (x) \in V$
51	50	eqvinc	$⊢ G (x) = F (x) \leftrightarrow \exists y (y = G (x) \land y = F (x))$
52	48 49 51	3imtr4g	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to (x (F^{-1} \circ G) x \to G (x) = F (x))$
53	52	adantlr	$⊢ (((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \land x \in A) \to (x (F^{-1} \circ G) x \to G (x) = F (x))$
54	19 53	mpd	$⊢ (((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \land x \in A) \to G (x) = F (x)$
55	8 11 54	eqfnfvd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \to G = F$
56	55	eqcomd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \to F = G$
57	56	ex	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (F^{-1} \circ G = {I ↾}_{A} \to F = G)$
58	5 57	impbid	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (F = G \leftrightarrow F^{-1} \circ G = {I ↾}_{A})$

Metamath Proof Explorer

Theorem f1eqcocnv

Proof