f1eqcocnv - Intuitionistic Logic Explorer

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

Theorem f1eqcocnv 5759

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 5462	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
2		coeq2 4762	. . . . 5 ⊢ (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐹) = (^◡𝐹 ∘ 𝐺))
3	2	eqeq1d 2174	. . . 4 ⊢ (𝐹 = 𝐺 → ((^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴) ↔ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
4	1, 3	syl5ibcom 154	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
5	4	adantr 274	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
6		f1fn 5395	. . . . . . 7 ⊢ (𝐺:𝐴–1-1→𝐵 → 𝐺 Fn 𝐴)
7	6	adantl 275	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → 𝐺 Fn 𝐴)
8	7	adantr 274	. . . . 5 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐺 Fn 𝐴)
9		f1fn 5395	. . . . . . 7 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
10	9	adantr 274	. . . . . 6 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → 𝐹 Fn 𝐴)
11	10	adantr 274	. . . . 5 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐹 Fn 𝐴)
12		equid 1689	. . . . . . . . . 10 ⊢ 𝑥 = 𝑥
13		resieq 4894	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥( I ↾ 𝐴)𝑥 ↔ 𝑥 = 𝑥))
14	12, 13	mpbiri 167	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥( I ↾ 𝐴)𝑥)
15	14	anidms 395	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → 𝑥( I ↾ 𝐴)𝑥)
16	15	adantl 275	. . . . . . 7 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥( I ↾ 𝐴)𝑥)
17		breq 3984	. . . . . . . 8 ⊢ ((^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ 𝑥( I ↾ 𝐴)𝑥))
18	17	ad2antlr 481	. . . . . . 7 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ 𝑥( I ↾ 𝐴)𝑥))
19	16, 18	mpbird 166	. . . . . 6 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥(^◡𝐹 ∘ 𝐺)𝑥)
20		vex 2729	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
21	20, 20	brco 4775	. . . . . . . . 9 ⊢ (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ ∃𝑦(𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥))
22		fnfun 5285	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 Fn 𝐴 → Fun 𝐺)
23	7, 22	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → Fun 𝐺)
24	23	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → Fun 𝐺)
25		fndm 5287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Fn 𝐴 → dom 𝐺 = 𝐴)
26	7, 25	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → dom 𝐺 = 𝐴)
27	26	eleq2d 2236	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝐴))
28	27	biimpar 295	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐺)
29		funopfvb 5530	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺) → ((𝐺‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
30	24, 28, 29	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
31	30	bicomd 140	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ↔ (𝐺‘𝑥) = 𝑦))
32		df-br 3983	. . . . . . . . . . . . 13 ⊢ (𝑥𝐺𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺)
33		eqcom 2167	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘𝑥) ↔ (𝐺‘𝑥) = 𝑦)
34	31, 32, 33	3bitr4g 222	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐺𝑦 ↔ 𝑦 = (𝐺‘𝑥)))
35	34	biimpd 143	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐺𝑦 → 𝑦 = (𝐺‘𝑥)))
36		df-br 3983	. . . . . . . . . . . . . 14 ⊢ (𝑥𝐹𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹)
37		fnfun 5285	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
38	10, 37	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → Fun 𝐹)
39	38	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → Fun 𝐹)
40		fndm 5287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
41	10, 40	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → dom 𝐹 = 𝐴)
42	41	eleq2d 2236	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
43	42	biimpar 295	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹)
44		funopfvb 5530	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
45	39, 43, 44	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
46	36, 45	bitr4id 198	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐹𝑦 ↔ (𝐹‘𝑥) = 𝑦))
47		vex 2729	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
48	47, 20	brcnv 4787	. . . . . . . . . . . . 13 ⊢ (𝑦^◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
49		eqcom 2167	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
50	46, 48, 49	3bitr4g 222	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑦^◡𝐹𝑥 ↔ 𝑦 = (𝐹‘𝑥)))
51	50	biimpd 143	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑦^◡𝐹𝑥 → 𝑦 = (𝐹‘𝑥)))
52	35, 51	anim12d 333	. . . . . . . . . 10 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥) → (𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
53	52	eximdv 1868	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (∃𝑦(𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥) → ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
54	21, 53	syl5bi 151	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
55	6	anim1i 338	. . . . . . . . . 10 ⊢ ((𝐺:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴))
56	55	adantll 468	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴))
57		funfvex 5503	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ V)
58	57	funfni 5288	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ V)
59		eqvincg 2850	. . . . . . . . 9 ⊢ ((𝐺‘𝑥) ∈ V → ((𝐺‘𝑥) = (𝐹‘𝑥) ↔ ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
60	56, 58, 59	3syl 17	. . . . . . . 8 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) = (𝐹‘𝑥) ↔ ∃𝑦(𝑦 = (𝐺‘𝑥) ∧ 𝑦 = (𝐹‘𝑥))))
61	54, 60	sylibrd 168	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → (𝐺‘𝑥) = (𝐹‘𝑥)))
62	61	adantlr 469	. . . . . 6 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → (𝐺‘𝑥) = (𝐹‘𝑥)))
63	19, 62	mpd 13	. . . . 5 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘𝑥))
64	8, 11, 63	eqfnfvd 5586	. . . 4 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐺 = 𝐹)
65	64	eqcomd 2171	. . 3 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐹 = 𝐺)
66	65	ex 114	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → ((^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴) → 𝐹 = 𝐺))
67	5, 66	impbid 128	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1343 ∃wex 1480 ∈ wcel 2136 Vcvv 2726 ⟨cop 3579 class class class wbr 3982 I cid 4266 ^◡ccnv 4603 dom cdm 4604 ↾ cres 4606 ∘ ccom 4608 Fun wfun 5182 Fn wfn 5183 –1-1→wf1 5185 ‘cfv 5188

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-pow 4153 ax-pr 4187

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ral 2449 df-rex 2450 df-v 2728 df-sbc 2952 df-csb 3046 df-un 3120 df-in 3122 df-ss 3129 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-br 3983 df-opab 4044 df-mpt 4045 df-id 4271 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196

This theorem is referenced by: (None)

W3C validator