Metamath Proof Explorer

Theorem fullpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same full functors. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fullpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
fullpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
fullpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
fullpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
fullpropd.a ⊢ φ → A ∈ V
fullpropd.b ⊢ φ → B ∈ V
fullpropd.c ⊢ φ → C ∈ V
fullpropd.d ⊢ φ → D ∈ V
Assertion fullpropd ⊢ φ → A Full C = B Full D

Proof

Step Hyp Ref Expression
1 fullpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
2 fullpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
3 fullpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
4 fullpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
5 fullpropd.a ⊢ φ → A ∈ V
6 fullpropd.b ⊢ φ → B ∈ V
7 fullpropd.c ⊢ φ → C ∈ V
8 fullpropd.d ⊢ φ → D ∈ V
9 relfull ⊢ Rel ⁡ A Full C
10 relfull ⊢ Rel ⁡ B Full D
11 1 homfeqbas ⊢ φ → Base A = Base B
12 11 adantr ⊢ φ ∧ f A Func C g → Base A = Base B
13 12 adantr ⊢ φ ∧ f A Func C g ∧ x ∈ Base A → Base A = Base B
14 eqid ⊢ Base C = Base C
15 eqid ⊢ Hom ⁡ C = Hom ⁡ C
16 eqid ⊢ Hom ⁡ D = Hom ⁡ D
17 3 ad3antrrr ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
18 eqid ⊢ Base A = Base A
19 simpllr ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → f A Func C g
20 18 14 19 funcf1 ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → f : Base A ⟶ Base C
21 simplr ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → x ∈ Base A
22 20 21 ffvelrnd ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → f ⁡ x ∈ Base C
23 simpr ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → y ∈ Base A
24 20 23 ffvelrnd ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → f ⁡ y ∈ Base C
25 14 15 16 17 22 24 homfeqval ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → f ⁡ x Hom ⁡ C f ⁡ y = f ⁡ x Hom ⁡ D f ⁡ y
26 25 eqeq2d ⊢ φ ∧ f A Func C g ∧ x ∈ Base A ∧ y ∈ Base A → ran ⁡ x g y = f ⁡ x Hom ⁡ C f ⁡ y ↔ ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
27 13 26 raleqbidva ⊢ φ ∧ f A Func C g ∧ x ∈ Base A → ∀ y ∈ Base A ran ⁡ x g y = f ⁡ x Hom ⁡ C f ⁡ y ↔ ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
28 12 27 raleqbidva ⊢ φ ∧ f A Func C g → ∀ x ∈ Base A ∀ y ∈ Base A ran ⁡ x g y = f ⁡ x Hom ⁡ C f ⁡ y ↔ ∀ x ∈ Base B ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
29 28 pm5.32da ⊢ φ → f A Func C g ∧ ∀ x ∈ Base A ∀ y ∈ Base A ran ⁡ x g y = f ⁡ x Hom ⁡ C f ⁡ y ↔ f A Func C g ∧ ∀ x ∈ Base B ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
30 1 2 3 4 5 6 7 8 funcpropd ⊢ φ → A Func C = B Func D
31 30 breqd ⊢ φ → f A Func C g ↔ f B Func D g
32 31 anbi1d ⊢ φ → f A Func C g ∧ ∀ x ∈ Base B ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y ↔ f B Func D g ∧ ∀ x ∈ Base B ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
33 29 32 bitrd ⊢ φ → f A Func C g ∧ ∀ x ∈ Base A ∀ y ∈ Base A ran ⁡ x g y = f ⁡ x Hom ⁡ C f ⁡ y ↔ f B Func D g ∧ ∀ x ∈ Base B ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
34 18 15 isfull ⊢ f A Full C g ↔ f A Func C g ∧ ∀ x ∈ Base A ∀ y ∈ Base A ran ⁡ x g y = f ⁡ x Hom ⁡ C f ⁡ y
35 eqid ⊢ Base B = Base B
36 35 16 isfull ⊢ f B Full D g ↔ f B Func D g ∧ ∀ x ∈ Base B ∀ y ∈ Base B ran ⁡ x g y = f ⁡ x Hom ⁡ D f ⁡ y
37 33 34 36 3bitr4g ⊢ φ → f A Full C g ↔ f B Full D g
38 9 10 37 eqbrrdiv ⊢ φ → A Full C = B Full D