f1eqcocnv - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > f1eqcocnv		GIF version

Theorem f1eqcocnv 5431

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	⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))

Proof of Theorem f1eqcocnv Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1cocnv1 5156	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
2		coeq2 4494	. . . . 5 ⊢ (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐹) = (^◡𝐹 ∘ 𝐺))
3	2	eqeq1d 2048	. . . 4 ⊢ (𝐹 = 𝐺 → ((^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴) ↔ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
4	1, 3	syl5ibcom 144	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
5	4	adantr 261	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
6		f1fn 5093	. . . . . . 7 ⊢ (𝐺:𝐴–1-1→𝐵 → 𝐺 Fn 𝐴)
7	6	adantl 262	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → 𝐺 Fn 𝐴)
8	7	adantr 261	. . . . 5 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐺 Fn 𝐴)
9		f1fn 5093	. . . . . . 7 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
10	9	adantr 261	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → 𝐹 Fn 𝐴)
11	10	adantr 261	. . . . 5 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐹 Fn 𝐴)
12		equid 1589	. . . . . . . . . 10 ⊢ 𝑥 = 𝑥
13		resieq 4622	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥( I ↾ 𝐴)𝑥 ↔ 𝑥 = 𝑥))
14	12, 13	mpbiri 157	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥( I ↾ 𝐴)𝑥)
15	14	anidms 377	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → 𝑥( I ↾ 𝐴)𝑥)
16	15	adantl 262	. . . . . . 7 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥( I ↾ 𝐴)𝑥)
17		breq 3766	. . . . . . . 8 ⊢ ((^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ 𝑥( I ↾ 𝐴)𝑥))
18	17	ad2antlr 458	. . . . . . 7 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ 𝑥( I ↾ 𝐴)𝑥))
19	16, 18	mpbird 156	. . . . . 6 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥(^◡𝐹 ∘ 𝐺)𝑥)
20		vex 2560	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
21	20, 20	brco 4506	. . . . . . . . 9 ⊢ (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ ∃𝑦(𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥))
22		fnfun 4996	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 Fn 𝐴 → Fun 𝐺)
23	7, 22	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → Fun 𝐺)
24	23	adantr 261	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → Fun 𝐺)
25		fndm 4998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Fn 𝐴 → dom 𝐺 = 𝐴)
26	7, 25	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → dom 𝐺 = 𝐴)
27	26	eleq2d 2107	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝐴))
28	27	biimpar 281	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐺)
29		funopfvb 5217	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺) → ((𝐺‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
30	24, 28, 29	syl2anc 391	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
31	30	bicomd 129	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ↔ (𝐺‘𝑥) = 𝑦))
32		df-br 3765	. . . . . . . . . . . . 13 ⊢ (𝑥𝐺𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺)
33		eqcom 2042	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘𝑥) ↔ (𝐺‘𝑥) = 𝑦)
34	31, 32, 33	3bitr4g 212	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐺𝑦 ↔ 𝑦 = (𝐺‘𝑥)))
35	34	biimpd 132	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐺𝑦 → 𝑦 = (𝐺‘𝑥)))
36		fnfun 4996	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
37	10, 36	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → Fun 𝐹)
38	37	adantr 261	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → Fun 𝐹)
39		fndm 4998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
40	10, 39	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → dom 𝐹 = 𝐴)
41	40	eleq2d 2107	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
42	41	biimpar 281	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹)
43		funopfvb 5217	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
44	38, 42, 43	syl2anc 391	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
45		df-br 3765	. . . . . . . . . . . . . 14 ⊢ (𝑥𝐹𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹)
46	44, 45	syl6rbbr 188	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐹𝑦 ↔ (𝐹‘𝑥) = 𝑦))
47		vex 2560	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
48	47, 20	brcnv 4518	. . . . . . . . . . . . 13 ⊢ (𝑦^◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
49		eqcom 2042	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
50	46, 48, 49	3bitr4g 212	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑦^◡𝐹𝑥 ↔ 𝑦 = (𝐹‘𝑥)))
51	50	biimpd 132	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑦^◡𝐹𝑥 → 𝑦 = (𝐹‘𝑥)))
52	35, 51	anim12d 318	. . . . . . . . . 10 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥) → (𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
53	52	eximdv 1760	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (∃𝑦(𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥) → ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
54	21, 53	syl5bi 141	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
55	6	anim1i 323	. . . . . . . . . 10 ⊢ ((𝐺:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴))
56	55	adantll 445	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴))
57		funfvex 5192	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ V)
58	57	funfni 4999	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ V)
59		eqvincg 2668	. . . . . . . . 9 ⊢ ((𝐺‘𝑥) ∈ V → ((𝐺‘𝑥) = (𝐹‘𝑥) ↔ ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
60	56, 58, 59	3syl 17	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) = (𝐹‘𝑥) ↔ ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
61	54, 60	sylibrd 158	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → (𝐺‘𝑥) = (𝐹‘𝑥)))
62	61	adantlr 446	. . . . . 6 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → (𝐺‘𝑥) = (𝐹‘𝑥)))
63	19, 62	mpd 13	. . . . 5 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘𝑥))
64	8, 11, 63	eqfnfvd 5268	. . . 4 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐺 = 𝐹)
65	64	eqcomd 2045	. . 3 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐹 = 𝐺)
66	65	ex 108	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → ((^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴) → 𝐹 = 𝐺))
67	5, 66	impbid 120	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 = wceq 1243 ∃wex 1381 ∈ wcel 1393 Vcvv 2557 ⟨cop 3378 class class class wbr 3764 I cid 4025 ^◡ccnv 4344 dom cdm 4345 ↾ cres 4347 ∘ ccom 4349 Fun wfun 4896 Fn wfn 4897 –1-1→wf1 4899 ‘cfv 4902

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 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 ax-pow 3927 ax-pr 3944

This theorem depends on definitions: df-bi 110 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 df-rex 2312 df-v 2559 df-sbc 2765 df-csb 2853 df-un 2922 df-in 2924 df-ss 2931 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-br 3765 df-opab 3819 df-mpt 3820 df-id 4030 df-xp 4351 df-rel 4352 df-cnv 4353 df-co 4354 df-dm 4355 df-rn 4356 df-res 4357 df-iota 4867 df-fun 4904 df-fn 4905 df-f 4906 df-f1 4907 df-fo 4908 df-f1o 4909 df-fv 4910

This theorem is referenced by: (None)

W3C validator