Theorem f1eqcocnv 5374

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 5099	. . . 4 ⊢ (𝐹:A–1-1→B → (◡𝐹 ∘ 𝐹) = ( I ↾ A))
2		coeq2 4437	. . . . 5 ⊢ (𝐹 = 𝐺 → (◡𝐹 ∘ 𝐹) = (◡𝐹 ∘ 𝐺))
3	2	eqeq1d 2045	. . . 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 5036	. . . . . . 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 5036	. . . . . . 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 1586	. . . . . . . . . 10 ⊢ x = x
13		resieq 4565	. . . . . . . . . 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 377	. . . . . . . 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 3757	. . . . . . . 8 ⊢ ((◡𝐹 ∘ 𝐺) = ( I ↾ A) → (x(◡𝐹 ∘ 𝐺)x ↔ x( I ↾ A)x))
18	17	ad2antlr 458	. . . . . . 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 2554	. . . . . . . . . 10 ⊢ x ∈ V
21	20, 20	brco 4449	. . . . . . . . 9 ⊢ (x(◡𝐹 ∘ 𝐺)x ↔ ∃y(x𝐺y ∧ y◡𝐹x))
22		fnfun 4939	. . . . . . . . . . . . . . . . 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 4941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Fn A → dom 𝐺 = A)
26	7, 25	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → dom 𝐺 = A)
27	26	eleq2d 2104	. . . . . . . . . . . . . . . 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 5160	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ x ∈ dom 𝐺) → ((𝐺‘x) = y ↔ ⟨x, y⟩ ∈ 𝐺))
30	24, 28, 29	syl2anc 391	. . . . . . . . . . . . . 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 3756	. . . . . . . . . . . . 13 ⊢ (x𝐺y ↔ ⟨x, y⟩ ∈ 𝐺)
33		eqcom 2039	. . . . . . . . . . . . 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 4939	. . . . . . . . . . . . . . . . 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 4941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn A → dom 𝐹 = A)
40	10, 39	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) → dom 𝐹 = A)
41	40	eleq2d 2104	. . . . . . . . . . . . . . . 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 5160	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ x ∈ dom 𝐹) → ((𝐹‘x) = y ↔ ⟨x, y⟩ ∈ 𝐹))
44	38, 42, 43	syl2anc 391	. . . . . . . . . . . . . 14 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → ((𝐹‘x) = y ↔ ⟨x, y⟩ ∈ 𝐹))
45		df-br 3756	. . . . . . . . . . . . . 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 2554	. . . . . . . . . . . . . 14 ⊢ y ∈ V
48	47, 20	brcnv 4461	. . . . . . . . . . . . 13 ⊢ (y◡𝐹x ↔ x𝐹y)
49		eqcom 2039	. . . . . . . . . . . . 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 1757	. . . . . . . . 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 445	. . . . . . . . 9 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → (𝐺 Fn A ∧ x ∈ A))
57		funfvex 5135	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ x ∈ dom 𝐺) → (𝐺‘x) ∈ V)
58	57	funfni 4942	. . . . . . . . 9 ⊢ ((𝐺 Fn A ∧ x ∈ A) → (𝐺‘x) ∈ V)
59		eqvincg 2662	. . . . . . . . 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 446	. . . . . 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 5211	. . . 4 ⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐺 = 𝐹)
65	64	eqcomd 2042	. . 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 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551  ⟨cop 3370   class class class wbr 3755   I cid 4016  ^◡ccnv 4287  dom cdm 4288   ↾ cres 4290   ∘ ccom 4292  Fun wfun 4839   Fn wfn 4840  –1-1→wf1 4842  ‘cfv 4845

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853

This theorem is referenced by: (None)