ffthiso - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ffthiso		Structured version Visualization version GIF version

Theorem ffthiso 17878

Description: A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.)

**Hypotheses**
Ref	Expression
fthmon.b	⊢ 𝐵 = (Base‘𝐶)
fthmon.h	⊢ 𝐻 = (Hom ‘𝐶)
fthmon.f	⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
fthmon.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
fthmon.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
fthmon.r	⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))
ffthiso.f	⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)
ffthiso.s	⊢ 𝐼 = (Iso‘𝐶)
ffthiso.t	⊢ 𝐽 = (Iso‘𝐷)

**Assertion**
Ref	Expression
ffthiso	⊢ (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))))

Proof of Theorem ffthiso Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fthmon.b	. . 3 ⊢ 𝐵 = (Base‘𝐶)
2		ffthiso.s	. . 3 ⊢ 𝐼 = (Iso‘𝐶)
3		ffthiso.t	. . 3 ⊢ 𝐽 = (Iso‘𝐷)
4		fthmon.f	. . . . 5 ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
5		fthfunc 17856	. . . . . 6 ⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷)
6	5	ssbri 5183	. . . . 5 ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 → 𝐹(𝐶 Func 𝐷)𝐺)
7	4, 6	syl 17	. . . 4 ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
8	7	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝐹(𝐶 Func 𝐷)𝐺)
9		fthmon.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ 𝐵)
11		fthmon.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
12	11	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ 𝐵)
13		simpr 484	. . 3 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝑅 ∈ (𝑋𝐼𝑌))
14	1, 2, 3, 8, 10, 12, 13	funciso 17820	. 2 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
15		eqid 2724	. . . 4 ⊢ (Inv‘𝐶) = (Inv‘𝐶)
16		df-br 5139	. . . . . . . 8 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
17	7, 16	sylib 217	. . . . . . 7 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
18		funcrcl 17809	. . . . . . 7 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
19	17, 18	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
20	19	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
21	20	ad3antrrr 727	. . . 4 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝐶 ∈ Cat)
22	9	ad3antrrr 727	. . . 4 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑋 ∈ 𝐵)
23	11	ad3antrrr 727	. . . 4 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑌 ∈ 𝐵)
24		eqid 2724	. . . . . . . . . . 11 ⊢ (Base‘𝐷) = (Base‘𝐷)
25		eqid 2724	. . . . . . . . . . 11 ⊢ (Inv‘𝐷) = (Inv‘𝐷)
26	19	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ Cat)
27	1, 24, 7	funcf1 17812	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐵⟶(Base‘𝐷))
28	27, 9	ffvelcdmd 7077	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑋) ∈ (Base‘𝐷))
29	27, 11	ffvelcdmd 7077	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑌) ∈ (Base‘𝐷))
30	24, 25, 26, 28, 29, 3	isoval 17708	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)))
31	30	eleq2d 2811	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))))
32	31	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)))
33	24, 25, 26, 28, 29	invfun 17707	. . . . . . . . . 10 ⊢ (𝜑 → Fun ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)))
34	33	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → Fun ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)))
35		funfvbrb 7042	. . . . . . . . 9 ⊢ (Fun ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)) → (((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅))))
36	34, 35	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → (((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅))))
37	32, 36	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)))
38	37	ad2antrr 723	. . . . . 6 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)))
39		simpr 484	. . . . . 6 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓))
40	38, 39	breqtrd 5164	. . . . 5 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑓))
41		fthmon.h	. . . . . 6 ⊢ 𝐻 = (Hom ‘𝐶)
42	4	ad3antrrr 727	. . . . . 6 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝐹(𝐶 Faith 𝐷)𝐺)
43		fthmon.r	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))
44	43	ad3antrrr 727	. . . . . 6 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅 ∈ (𝑋𝐻𝑌))
45		simplr 766	. . . . . 6 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑓 ∈ (𝑌𝐻𝑋))
46	1, 41, 42, 22, 23, 44, 45, 15, 25	fthinv 17875	. . . . 5 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → (𝑅(𝑋(Inv‘𝐶)𝑌)𝑓 ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑓)))
47	40, 46	mpbird 257	. . . 4 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅(𝑋(Inv‘𝐶)𝑌)𝑓)
48	1, 15, 21, 22, 23, 2, 47	inviso1 17709	. . 3 ⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅 ∈ (𝑋𝐼𝑌))
49		eqid 2724	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
50		ffthiso.f	. . . . 5 ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)
51	50	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝐹(𝐶 Full 𝐷)𝐺)
52	11	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝑌 ∈ 𝐵)
53	9	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝑋 ∈ 𝐵)
54	24, 49, 3, 26, 29, 28	isohom 17719	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝑌)𝐽(𝐹‘𝑋)) ⊆ ((𝐹‘𝑌)(Hom ‘𝐷)(𝐹‘𝑋)))
55	54	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ((𝐹‘𝑌)𝐽(𝐹‘𝑋)) ⊆ ((𝐹‘𝑌)(Hom ‘𝐷)(𝐹‘𝑋)))
56	24, 25, 26, 28, 29, 3	invf 17711	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)):((𝐹‘𝑋)𝐽(𝐹‘𝑌))⟶((𝐹‘𝑌)𝐽(𝐹‘𝑋)))
57	56	ffvelcdmda 7076	. . . . 5 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) ∈ ((𝐹‘𝑌)𝐽(𝐹‘𝑋)))
58	55, 57	sseldd 3975	. . . 4 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) ∈ ((𝐹‘𝑌)(Hom ‘𝐷)(𝐹‘𝑋)))
59	1, 49, 41, 51, 52, 53, 58	fulli 17862	. . 3 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ∃𝑓 ∈ (𝑌𝐻𝑋)(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓))
60	48, 59	r19.29a 3154	. 2 ⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝑅 ∈ (𝑋𝐼𝑌))
61	14, 60	impbida 798	1 ⊢ (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ⊆ wss 3940 ⟨cop 4626 class class class wbr 5138 dom cdm 5666 Fun wfun 6527 ‘cfv 6533 (class class class)co 7401 Basecbs 17140 Hom chom 17204 Catccat 17604 Invcinv 17688 Isociso 17689 Func cfunc 17800 Full cful 17851 Faith cfth 17852

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-1st 7968 df-2nd 7969 df-map 8817 df-ixp 8887 df-cat 17608 df-cid 17609 df-sect 17690 df-inv 17691 df-iso 17692 df-func 17804 df-full 17853 df-fth 17854

This theorem is referenced by: (None)

W3C validator