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

Theorem cofth 16806
Description: The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
Hypotheses
Ref Expression
cofth.f (𝜑𝐹 ∈ (𝐶 Faith 𝐷))
cofth.g (𝜑𝐺 ∈ (𝐷 Faith 𝐸))
Assertion
Ref Expression
cofth (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Faith 𝐸))

Proof of Theorem cofth
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 16733 . . 3 Rel (𝐶 Func 𝐸)
2 fthfunc 16778 . . . . 5 (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷)
3 cofth.f . . . . 5 (𝜑𝐹 ∈ (𝐶 Faith 𝐷))
42, 3sseldi 3807 . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
5 fthfunc 16778 . . . . 5 (𝐷 Faith 𝐸) ⊆ (𝐷 Func 𝐸)
6 cofth.g . . . . 5 (𝜑𝐺 ∈ (𝐷 Faith 𝐸))
75, 6sseldi 3807 . . . 4 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
84, 7cofucl 16759 . . 3 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Func 𝐸))
9 1st2nd 7453 . . 3 ((Rel (𝐶 Func 𝐸) ∧ (𝐺func 𝐹) ∈ (𝐶 Func 𝐸)) → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
101, 8, 9sylancr 577 . 2 (𝜑 → (𝐺func 𝐹) = ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩)
11 1st2ndbr 7456 . . . . 5 ((Rel (𝐶 Func 𝐸) ∧ (𝐺func 𝐹) ∈ (𝐶 Func 𝐸)) → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
121, 8, 11sylancr 577 . . . 4 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)))
13 eqid 2817 . . . . . . . 8 (Base‘𝐷) = (Base‘𝐷)
14 eqid 2817 . . . . . . . 8 (Hom ‘𝐷) = (Hom ‘𝐷)
15 eqid 2817 . . . . . . . 8 (Hom ‘𝐸) = (Hom ‘𝐸)
16 relfth 16780 . . . . . . . . 9 Rel (𝐷 Faith 𝐸)
176adantr 468 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Faith 𝐸))
18 1st2ndbr 7456 . . . . . . . . 9 ((Rel (𝐷 Faith 𝐸) ∧ 𝐺 ∈ (𝐷 Faith 𝐸)) → (1st𝐺)(𝐷 Faith 𝐸)(2nd𝐺))
1916, 17, 18sylancr 577 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐷 Faith 𝐸)(2nd𝐺))
20 eqid 2817 . . . . . . . . . 10 (Base‘𝐶) = (Base‘𝐶)
21 relfunc 16733 . . . . . . . . . . 11 Rel (𝐶 Func 𝐷)
224adantr 468 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
23 1st2ndbr 7456 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2421, 22, 23sylancr 577 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2520, 13, 24funcf1 16737 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26 simprl 778 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
2725, 26ffvelrnd 6589 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
28 simprr 780 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
2925, 28ffvelrnd 6589 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
3013, 14, 15, 19, 27, 29fthf1 16788 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))–1-1→(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
31 eqid 2817 . . . . . . . 8 (Hom ‘𝐶) = (Hom ‘𝐶)
32 relfth 16780 . . . . . . . . 9 Rel (𝐶 Faith 𝐷)
333adantr 468 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Faith 𝐷))
34 1st2ndbr 7456 . . . . . . . . 9 ((Rel (𝐶 Faith 𝐷) ∧ 𝐹 ∈ (𝐶 Faith 𝐷)) → (1st𝐹)(𝐶 Faith 𝐷)(2nd𝐹))
3532, 33, 34sylancr 577 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Faith 𝐷)(2nd𝐹))
3620, 31, 14, 35, 26, 28fthf1 16788 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
37 f1co 6333 . . . . . . 7 (((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))–1-1→(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))) ∧ (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
3830, 36, 37syl2anc 575 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
397adantr 468 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
4020, 22, 39, 26, 28cofu2nd 16756 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
41 eqidd 2818 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑦))
4220, 22, 39, 26cofu1 16755 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑥) = ((1st𝐺)‘((1st𝐹)‘𝑥)))
4320, 22, 39, 28cofu1 16755 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺func 𝐹))‘𝑦) = ((1st𝐺)‘((1st𝐹)‘𝑦)))
4442, 43oveq12d 6899 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) = (((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦))))
4540, 41, 44f1eq123d 6354 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(2nd ‘(𝐺func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)) ↔ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st𝐺)‘((1st𝐹)‘𝑥))(Hom ‘𝐸)((1st𝐺)‘((1st𝐹)‘𝑦)))))
4638, 45mpbird 248 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
4746ralrimivva 3170 . . . 4 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦)))
4820, 31, 15isfth2 16786 . . . 4 ((1st ‘(𝐺func 𝐹))(𝐶 Faith 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ((1st ‘(𝐺func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺func 𝐹)) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺func 𝐹))‘𝑦))))
4912, 47, 48sylanbrc 574 . . 3 (𝜑 → (1st ‘(𝐺func 𝐹))(𝐶 Faith 𝐸)(2nd ‘(𝐺func 𝐹)))
50 df-br 4856 . . 3 ((1st ‘(𝐺func 𝐹))(𝐶 Faith 𝐸)(2nd ‘(𝐺func 𝐹)) ↔ ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Faith 𝐸))
5149, 50sylib 209 . 2 (𝜑 → ⟨(1st ‘(𝐺func 𝐹)), (2nd ‘(𝐺func 𝐹))⟩ ∈ (𝐶 Faith 𝐸))
5210, 51eqeltrd 2896 1 (𝜑 → (𝐺func 𝐹) ∈ (𝐶 Faith 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2157  wral 3107  cop 4387   class class class wbr 4855  ccom 5326  Rel wrel 5327  1-1wf1 6105  cfv 6108  (class class class)co 6881  1st c1st 7403  2nd c2nd 7404  Basecbs 16075  Hom chom 16171   Func cfunc 16725  func ccofu 16727   Faith cfth 16774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5230  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-1st 7405  df-2nd 7406  df-map 8101  df-ixp 8153  df-cat 16540  df-cid 16541  df-func 16729  df-cofu 16731  df-fth 16776
This theorem is referenced by:  coffth  16807
  Copyright terms: Public domain W3C validator