foeqcnvco

Description: Condition for function equality in terms of vanishing of the composition with the converse.EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fococnv2	$⊢ F : A \underset{onto}{⟶} B \to F \circ F^{-1} = {I ↾}_{B}$
2		cnveq	$⊢ F = G \to F^{-1} = G^{-1}$
3	2	coeq2d	$⊢ F = G \to F \circ F^{-1} = F \circ G^{-1}$
4	3	eqeq1d	$⊢ F = G \to (F \circ F^{-1} = {I ↾}_{B} \leftrightarrow F \circ G^{-1} = {I ↾}_{B})$
5	1 4	syl5ibcom	$⊢ F : A \underset{onto}{⟶} B \to (F = G \to F \circ G^{-1} = {I ↾}_{B})$
6	5	adantr	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to (F = G \to F \circ G^{-1} = {I ↾}_{B})$
7		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
8	7	ad2antrr	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \to F Fn A$
9		fofn	$⊢ G : A \underset{onto}{⟶} B \to G Fn A$
10	9	ad2antlr	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \to G Fn A$
11	9	adantl	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to G Fn A$
12		fnopfv	$⊢ (G Fn A \land x \in A) \to ⟨x, G (x)⟩ \in G$
13	11 12	sylan	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to ⟨x, G (x)⟩ \in G$
14		fvex	$⊢ G (x) \in V$
15		vex	$⊢ x \in V$
16	14 15	brcnv	$⊢ G (x) G^{-1} x \leftrightarrow x G G (x)$
17		df-br	$⊢ x G G (x) \leftrightarrow ⟨x, G (x)⟩ \in G$
18	16 17	bitri	$⊢ G (x) G^{-1} x \leftrightarrow ⟨x, G (x)⟩ \in G$
19	13 18	sylibr	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to G (x) G^{-1} x$
20	7	adantr	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to F Fn A$
21		fnopfv	$⊢ (F Fn A \land x \in A) \to ⟨x, F (x)⟩ \in F$
22	20 21	sylan	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to ⟨x, F (x)⟩ \in F$
23		df-br	$⊢ x F F (x) \leftrightarrow ⟨x, F (x)⟩ \in F$
24	22 23	sylibr	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to x F F (x)$
25		breq2	$⊢ y = x \to (G (x) G^{-1} y \leftrightarrow G (x) G^{-1} x)$
26		breq1	$⊢ y = x \to (y F F (x) \leftrightarrow x F F (x))$
27	25 26	anbi12d	$⊢ y = x \to ((G (x) G^{-1} y \land y F F (x)) \leftrightarrow (G (x) G^{-1} x \land x F F (x)))$
28	15 27	spcev	$⊢ (G (x) G^{-1} x \land x F F (x)) \to \exists y (G (x) G^{-1} y \land y F F (x))$
29	19 24 28	syl2anc	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to \exists y (G (x) G^{-1} y \land y F F (x))$
30		fvex	$⊢ F (x) \in V$
31	14 30	brco	$⊢ G (x) (F \circ G^{-1}) F (x) \leftrightarrow \exists y (G (x) G^{-1} y \land y F F (x))$
32	29 31	sylibr	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to G (x) (F \circ G^{-1}) F (x)$
33	32	adantlr	$⊢ (((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \land x \in A) \to G (x) (F \circ G^{-1}) F (x)$
34		breq	$⊢ F \circ G^{-1} = {I ↾}_{B} \to (G (x) (F \circ G^{-1}) F (x) \leftrightarrow G (x) ({I ↾}_{B}) F (x))$
35	34	ad2antlr	$⊢ (((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \land x \in A) \to (G (x) (F \circ G^{-1}) F (x) \leftrightarrow G (x) ({I ↾}_{B}) F (x))$
36	33 35	mpbid	$⊢ (((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \land x \in A) \to G (x) ({I ↾}_{B}) F (x)$
37		fof	$⊢ G : A \underset{onto}{⟶} B \to G : A ⟶ B$
38	37	adantl	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to G : A ⟶ B$
39	38	ffvelcdmda	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to G (x) \in B$
40		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
41	40	adantr	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to F : A ⟶ B$
42	41	ffvelcdmda	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to F (x) \in B$
43		resieq	$⊢ (G (x) \in B \land F (x) \in B) \to (G (x) ({I ↾}_{B}) F (x) \leftrightarrow G (x) = F (x))$
44	39 42 43	syl2anc	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land x \in A) \to (G (x) ({I ↾}_{B}) F (x) \leftrightarrow G (x) = F (x))$
45	44	adantlr	$⊢ (((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \land x \in A) \to (G (x) ({I ↾}_{B}) F (x) \leftrightarrow G (x) = F (x))$
46	36 45	mpbid	$⊢ (((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \land x \in A) \to G (x) = F (x)$
47	46	eqcomd	$⊢ (((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \land x \in A) \to F (x) = G (x)$
48	8 10 47	eqfnfvd	$⊢ ((F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \land F \circ G^{-1} = {I ↾}_{B}) \to F = G$
49	48	ex	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to (F \circ G^{-1} = {I ↾}_{B} \to F = G)$
50	6 49	impbid	$⊢ (F : A \underset{onto}{⟶} B \land G : A \underset{onto}{⟶} B) \to (F = G \leftrightarrow F \circ G^{-1} = {I ↾}_{B})$

Metamath Proof Explorer

Theorem foeqcnvco

Proof