f1eqcocnv - Intuitionistic Logic Explorer

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

Theorem f1eqcocnv 5770

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 5472	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
2		coeq2 4769	. . . . 5 ⊢ (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐹) = (^◡𝐹 ∘ 𝐺))
3	2	eqeq1d 2179	. . . 4 ⊢ (𝐹 = 𝐺 → ((^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴) ↔ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
4	1, 3	syl5ibcom 154	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
5	4	adantr 274	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 → (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
6		f1fn 5405	. . . . . . 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 5405	. . . . . . 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 1694	. . . . . . . . . 10 ⊢ 𝑥 = 𝑥
13		resieq 4901	. . . . . . . . . 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 3991	. . . . . . . 8 ⊢ ((^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ 𝑥( I ↾ 𝐴)𝑥))
18	17	ad2antlr 486	. . . . . . 7 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ 𝑥( I ↾ 𝐴)𝑥))
19	16, 18	mpbird 166	. . . . . 6 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥(^◡𝐹 ∘ 𝐺)𝑥)
20		vex 2733	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
21	20, 20	brco 4782	. . . . . . . . 9 ⊢ (𝑥(^◡𝐹 ∘ 𝐺)𝑥 ↔ ∃𝑦(𝑥𝐺𝑦 ∧ 𝑦^◡𝐹𝑥))
22		fnfun 5295	. . . . . . . . . . . . . . . . 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 5297	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Fn 𝐴 → dom 𝐺 = 𝐴)
26	7, 25	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → dom 𝐺 = 𝐴)
27	26	eleq2d 2240	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝐴))
28	27	biimpar 295	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐺)
29		funopfvb 5540	. . . . . . . . . . . . . . 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 3990	. . . . . . . . . . . . 13 ⊢ (𝑥𝐺𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺)
33		eqcom 2172	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘𝑥) ↔ (𝐺‘𝑥) = 𝑦)
34	31, 32, 33	3bitr4g 222	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐺𝑦 ↔ 𝑦 = (𝐺‘𝑥)))
35	34	biimpd 143	. . . . . . . . . . 11 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥𝐺𝑦 → 𝑦 = (𝐺‘𝑥)))
36		df-br 3990	. . . . . . . . . . . . . 14 ⊢ (𝑥𝐹𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹)
37		fnfun 5295	. . . . . . . . . . . . . . . . 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 5297	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
41	10, 40	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → dom 𝐹 = 𝐴)
42	41	eleq2d 2240	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
43	42	biimpar 295	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹)
44		funopfvb 5540	. . . . . . . . . . . . . . 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 2733	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
48	47, 20	brcnv 4794	. . . . . . . . . . . . 13 ⊢ (𝑦^◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
49		eqcom 2172	. . . . . . . . . . . . 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 1873	. . . . . . . . 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 473	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴))
57		funfvex 5513	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ V)
58	57	funfni 5298	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ V)
59		eqvincg 2854	. . . . . . . . 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 474	. . . . . 6 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑥(^◡𝐹 ∘ 𝐺)𝑥 → (𝐺‘𝑥) = (𝐹‘𝑥)))
63	19, 62	mpd 13	. . . . 5 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘𝑥))
64	8, 11, 63	eqfnfvd 5596	. . . 4 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (^◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)) → 𝐺 = 𝐹)
65	64	eqcomd 2176	. . 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 1348 ∃wex 1485 ∈ wcel 2141 Vcvv 2730 ⟨cop 3586 class class class wbr 3989 I cid 4273 ^◡ccnv 4610 dom cdm 4611 ↾ cres 4613 ∘ ccom 4615 Fun wfun 5192 Fn wfn 5193 –1-1→wf1 5195 ‘cfv 5198

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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194

This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-v 2732 df-sbc 2956 df-csb 3050 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-br 3990 df-opab 4051 df-mpt 4052 df-id 4278 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206

This theorem is referenced by: (None)

W3C validator