Theorem f1eqcocnv 5352

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

Assertion

Ref	Expression
f1eqcocnv	⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ A)))

Proof of Theorem f1eqcocnv

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1cocnv1 5077	. . . 4 ⊢ (𝐹:A–1-1→B → (◡𝐹 ∘ 𝐹) = ( I ↾ A))
2		coeq2 4417	. . . . 5 ⊢ (𝐹 = 𝐺 → (◡𝐹 ∘ 𝐹) = (◡𝐹 ∘ 𝐺))
3	2	eqeq1d 2026	. . . 4 ⊢ (𝐹 = 𝐺 → ((◡𝐹 ∘ 𝐹) = ( I ↾ A) ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ A)))
4	1, 3	syl5ibcom 144	. . 3 ⊢ (𝐹:A–1-1→B → (𝐹 = 𝐺 → (◡𝐹 ∘ 𝐺) = ( I ↾ A)))
5	4	adantr 261	. 2 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → (𝐹 = 𝐺 → (◡𝐹 ∘ 𝐺) = ( I ↾ A)))
6		f1fn 5014	. . . . . . 7 ⊢ (𝐺:A–1-1→B → 𝐺 Fn A)
7	6	adantl 262	. . . . . 6 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → 𝐺 Fn A)
8	7	adantr 261	. . . . 5 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐺 Fn A)
9		f1fn 5014	. . . . . . 7 ⊢ (𝐹:A–1-1→B → 𝐹 Fn A)
10	9	adantr 261	. . . . . 6 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → 𝐹 Fn A)
11	10	adantr 261	. . . . 5 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐹 Fn A)
12		equid 1567	. . . . . . . . . 10 ⊢ x = x
13		resieq 4545	. . . . . . . . . 10 ⊢ ((x ∈ A ∧ x ∈ A) → (x( I ↾ A)x ↔ x = x))
14	12, 13	mpbiri 157	. . . . . . . . 9 ⊢ ((x ∈ A ∧ x ∈ A) → x( I ↾ A)x)
15	14	anidms 379	. . . . . . . 8 ⊢ (x ∈ A → x( I ↾ A)x)
16	15	adantl 262	. . . . . . 7 ⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → x( I ↾ A)x)
17		breq 3736	. . . . . . . 8 ⊢ ((◡𝐹 ∘ 𝐺) = ( I ↾ A) → (x(◡𝐹 ∘ 𝐺)x ↔ x( I ↾ A)x))
18	17	ad2antlr 462	. . . . . . 7 ⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → (x(◡𝐹 ∘ 𝐺)x ↔ x( I ↾ A)x))
19	16, 18	mpbird 156	. . . . . 6 ⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → x(◡𝐹 ∘ 𝐺)x)
20		vex 2534	. . . . . . . . . 10 ⊢ x ∈ V
21	20, 20	brco 4429	. . . . . . . . 9 ⊢ (x(◡𝐹 ∘ 𝐺)x ↔ ∃y(x𝐺y ∧ y◡𝐹x))
22		fnfun 4918	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 Fn A → Fun 𝐺)
23	7, 22	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → Fun 𝐺)
24	23	adantr 261	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → Fun 𝐺)
25		fndm 4920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Fn A → dom 𝐺 = A)
26	7, 25	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → dom 𝐺 = A)
27	26	eleq2d 2085	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → (x ∈ dom 𝐺 ↔ x ∈ A))
28	27	biimpar 281	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → x ∈ dom 𝐺)
29		funopfvb 5138	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ x ∈ dom 𝐺) → ((𝐺‘x) = y ↔ ⟨x, y⟩ ∈ 𝐺))
30	24, 28, 29	syl2anc 393	. . . . . . . . . . . . . 14 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → ((𝐺‘x) = y ↔ ⟨x, y⟩ ∈ 𝐺))
31	30	bicomd 129	. . . . . . . . . . . . 13 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (⟨x, y⟩ ∈ 𝐺 ↔ (𝐺‘x) = y))
32		df-br 3735	. . . . . . . . . . . . 13 ⊢ (x𝐺y ↔ ⟨x, y⟩ ∈ 𝐺)
33		eqcom 2020	. . . . . . . . . . . . 13 ⊢ (y = (𝐺‘x) ↔ (𝐺‘x) = y)
34	31, 32, 33	3bitr4g 212	. . . . . . . . . . . 12 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (x𝐺y ↔ y = (𝐺‘x)))
35	34	biimpd 132	. . . . . . . . . . 11 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (x𝐺y → y = (𝐺‘x)))
36		fnfun 4918	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn A → Fun 𝐹)
37	10, 36	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → Fun 𝐹)
38	37	adantr 261	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → Fun 𝐹)
39		fndm 4920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn A → dom 𝐹 = A)
40	10, 39	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → dom 𝐹 = A)
41	40	eleq2d 2085	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → (x ∈ dom 𝐹 ↔ x ∈ A))
42	41	biimpar 281	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → x ∈ dom 𝐹)
43		funopfvb 5138	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ x ∈ dom 𝐹) → ((𝐹‘x) = y ↔ ⟨x, y⟩ ∈ 𝐹))
44	38, 42, 43	syl2anc 393	. . . . . . . . . . . . . 14 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → ((𝐹‘x) = y ↔ ⟨x, y⟩ ∈ 𝐹))
45		df-br 3735	. . . . . . . . . . . . . 14 ⊢ (x𝐹y ↔ ⟨x, y⟩ ∈ 𝐹)
46	44, 45	syl6rbbr 188	. . . . . . . . . . . . 13 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (x𝐹y ↔ (𝐹‘x) = y))
47		vex 2534	. . . . . . . . . . . . . 14 ⊢ y ∈ V
48	47, 20	brcnv 4441	. . . . . . . . . . . . 13 ⊢ (y◡𝐹x ↔ x𝐹y)
49		eqcom 2020	. . . . . . . . . . . . 13 ⊢ (y = (𝐹‘x) ↔ (𝐹‘x) = y)
50	46, 48, 49	3bitr4g 212	. . . . . . . . . . . 12 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (y◡𝐹x ↔ y = (𝐹‘x)))
51	50	biimpd 132	. . . . . . . . . . 11 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (y◡𝐹x → y = (𝐹‘x)))
52	35, 51	anim12d 318	. . . . . . . . . 10 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → ((x𝐺y ∧ y◡𝐹x) → (y = (𝐺‘x) ∧ y = (𝐹‘x))))
53	52	eximdv 1738	. . . . . . . . 9 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (∃y(x𝐺y ∧ y◡𝐹x) → ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x))))
54	21, 53	syl5bi 141	. . . . . . . 8 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (x(◡𝐹 ∘ 𝐺)x → ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x))))
55	6	anim1i 323	. . . . . . . . . 10 ⊢ ((𝐺:A–1-1→B ∧ x ∈ A) → (𝐺 Fn A ∧ x ∈ A))
56	55	adantll 448	. . . . . . . . 9 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (𝐺 Fn A ∧ x ∈ A))
57		funfvex 5113	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ x ∈ dom 𝐺) → (𝐺‘x) ∈ V)
58	57	funfni 4921	. . . . . . . . 9 ⊢ ((𝐺 Fn A ∧ x ∈ A) → (𝐺‘x) ∈ V)
59		eqvincg 2641	. . . . . . . . 9 ⊢ ((𝐺‘x) ∈ V → ((𝐺‘x) = (𝐹‘x) ↔ ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x))))
60	56, 58, 59	3syl 17	. . . . . . . 8 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → ((𝐺‘x) = (𝐹‘x) ↔ ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x))))
61	54, 60	sylibrd 158	. . . . . . 7 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (x(◡𝐹 ∘ 𝐺)x → (𝐺‘x) = (𝐹‘x)))
62	61	adantlr 449	. . . . . 6 ⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → (x(◡𝐹 ∘ 𝐺)x → (𝐺‘x) = (𝐹‘x)))
63	19, 62	mpd 13	. . . . 5 ⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → (𝐺‘x) = (𝐹‘x))
64	8, 11, 63	eqfnfvd 5189	. . . 4 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐺 = 𝐹)
65	64	eqcomd 2023	. . 3 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐹 = 𝐺)
66	65	ex 108	. 2 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → ((◡𝐹 ∘ 𝐺) = ( I ↾ A) → 𝐹 = 𝐺))
67	5, 66	impbid 120	1 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ A)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1226  ∃wex 1358   ∈ wcel 1370  Vcvv 2531  ⟨cop 3349   class class class wbr 3734   I cid 3995  ^◡ccnv 4267  dom cdm 4268   ↾ cres 4270   ∘ ccom 4272  Fun wfun 4819   Fn wfn 4820  –1-1→wf1 4822  ‘cfv 4825

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-sbc 2738  df-csb 2826  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-mpt 3790  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-fo 4831  df-f1o 4832  df-fv 4833

This theorem is referenced by: (None)