f1eqcocnvOLD

Description: Obsolete version of f1eqcocnv as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	f1eqcocnvOLD	$⊢ (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		fndm	$⊢ G Fn A \to dom G = A$
23	7 22	syl	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to dom G = A$
24	23	eleq2d	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (x \in dom G \leftrightarrow x \in A)$
25	24	biimpar	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to x \in dom G$
26		funopfvb	$⊢ (Fun G \land x \in dom G) \to (G (x) = y \leftrightarrow ⟨x, y⟩ \in G)$
27	21 25 26	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)$
28	27	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)$
29		df-br	$⊢ x G y \leftrightarrow ⟨x, y⟩ \in G$
30		eqcom	$⊢ y = G (x) \leftrightarrow G (x) = y$
31	28 29 30	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))$
32	31	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))$
33		df-br	$⊢ x F y \leftrightarrow ⟨x, y⟩ \in F$
34		fnfun	$⊢ F Fn A \to Fun F$
35	10 34	syl	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to Fun F$
36		fndm	$⊢ F Fn A \to dom F = A$
37	10 36	syl	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to dom F = A$
38	37	eleq2d	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (x \in dom F \leftrightarrow x \in A)$
39	38	biimpar	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land x \in A) \to x \in dom F$
40		funopfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow ⟨x, y⟩ \in F)$
41	35 39 40	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)$
42	33 41	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)$
43		vex	$⊢ y \in V$
44		vex	$⊢ x \in V$
45	43 44	brcnv	$⊢ y F^{-1} x \leftrightarrow x F y$
46		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
47	42 45 46	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))$
48	47	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))$
49	32 48	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)))$
50	49	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)))$
51	44 44	brco	$⊢ x (F^{-1} \circ G) x \leftrightarrow \exists y (x G y \land y F^{-1} x)$
52		fvex	$⊢ G (x) \in V$
53	52	eqvinc	$⊢ G (x) = F (x) \leftrightarrow \exists y (y = G (x) \land y = F (x))$
54	50 51 53	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))$
55	54	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))$
56	19 55	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)$
57	8 11 56	eqfnfvd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \to G = F$
58	57	eqcomd	$⊢ ((F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \land F^{-1} \circ G = {I ↾}_{A}) \to F = G$
59	58	ex	$⊢ (F : A \underset{1-1}{⟶} B \land G : A \underset{1-1}{⟶} B) \to (F^{-1} \circ G = {I ↾}_{A} \to F = G)$
60	5 59	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 f1eqcocnvOLD

Proof