Metamath Proof Explorer

Theorem fullres2c

Description: Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017)

Ref Expression
Hypotheses ffthres2c.a ⊢ A = Base C
ffthres2c.e ⊢ E = D ↾ 𝑠 S
ffthres2c.d ⊢ φ → D ∈ Cat
ffthres2c.r ⊢ φ → S ∈ V
ffthres2c.1 ⊢ φ → F : A ⟶ S
Assertion fullres2c ⊢ φ → F C Full D G ↔ F C Full E G

Proof

Step Hyp Ref Expression
1 ffthres2c.a ⊢ A = Base C
2 ffthres2c.e ⊢ E = D ↾ 𝑠 S
3 ffthres2c.d ⊢ φ → D ∈ Cat
4 ffthres2c.r ⊢ φ → S ∈ V
5 ffthres2c.1 ⊢ φ → F : A ⟶ S
6 1 2 3 4 5 funcres2c ⊢ φ → F C Func D G ↔ F C Func E G
7 eqid ⊢ Hom ⁡ D = Hom ⁡ D
8 2 7 resshom ⊢ S ∈ V → Hom ⁡ D = Hom ⁡ E
9 4 8 syl ⊢ φ → Hom ⁡ D = Hom ⁡ E
10 9 oveqd ⊢ φ → F ⁡ x Hom ⁡ D F ⁡ y = F ⁡ x Hom ⁡ E F ⁡ y
11 10 eqeq2d ⊢ φ → ran ⁡ x G y = F ⁡ x Hom ⁡ D F ⁡ y ↔ ran ⁡ x G y = F ⁡ x Hom ⁡ E F ⁡ y
12 11 2ralbidv ⊢ φ → ∀ x ∈ A ∀ y ∈ A ran ⁡ x G y = F ⁡ x Hom ⁡ D F ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A ran ⁡ x G y = F ⁡ x Hom ⁡ E F ⁡ y
13 6 12 anbi12d ⊢ φ → F C Func D G ∧ ∀ x ∈ A ∀ y ∈ A ran ⁡ x G y = F ⁡ x Hom ⁡ D F ⁡ y ↔ F C Func E G ∧ ∀ x ∈ A ∀ y ∈ A ran ⁡ x G y = F ⁡ x Hom ⁡ E F ⁡ y
14 1 7 isfull ⊢ F C Full D G ↔ F C Func D G ∧ ∀ x ∈ A ∀ y ∈ A ran ⁡ x G y = F ⁡ x Hom ⁡ D F ⁡ y
15 eqid ⊢ Hom ⁡ E = Hom ⁡ E
16 1 15 isfull ⊢ F C Full E G ↔ F C Func E G ∧ ∀ x ∈ A ∀ y ∈ A ran ⁡ x G y = F ⁡ x Hom ⁡ E F ⁡ y
17 13 14 16 3bitr4g ⊢ φ → F C Full D G ↔ F C Full E G