Metamath Proof Explorer

Theorem funcres2c

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

Ref Expression
Hypotheses funcres2c.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
funcres2c.e ⊢ 𝐸 = ( 𝐷 ↾s 𝑆 )
funcres2c.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
funcres2c.r ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
funcres2c.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
Assertion funcres2c ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 funcres2c.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
2 funcres2c.e ⊢ 𝐸 = ( 𝐷 ↾s 𝑆 )
3 funcres2c.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 funcres2c.r ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5 funcres2c.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
6 orc ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) )
7 6 a1i ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) )
8 olc ⊢ ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) )
9 8 a1i ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) )
10 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12 eqid ⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 )
13 inss2 ⊢ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ⊆ ( Base ‘ 𝐷 )
14 13 a1i ⊢ ( 𝜑 → ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ⊆ ( Base ‘ 𝐷 ) )
15 11 12 3 14 fullsubc ⊢ ( 𝜑 → ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ∈ ( Subcat ‘ 𝐷 ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ∈ ( Subcat ‘ 𝐷 ) )
17 12 11 homffn ⊢ ( Homf ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) )
18 xpss12 ⊢ ( ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ⊆ ( Base ‘ 𝐷 ) ∧ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ⊆ ( Base ‘ 𝐷 ) ) → ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ⊆ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
19 13 13 18 mp2an ⊢ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ⊆ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) )
20 fnssres ⊢ ( ( ( Homf ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ∧ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ⊆ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) Fn ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) )
21 17 19 20 mp2an ⊢ ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) Fn ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
22 21 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) Fn ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) )
23 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → 𝐹 : 𝐴 ⟶ 𝑆 )
24 23 ffnd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → 𝐹 Fn 𝐴 )
25 23 frnd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ran 𝐹 ⊆ 𝑆 )
26 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
27 1 11 26 funcf1 ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐷 ) )
28 27 frnd ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ran 𝐹 ⊆ ( Base ‘ 𝐷 ) )
29 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
30 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 )
31 1 29 30 funcf1 ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐸 ) )
32 31 frnd ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ran 𝐹 ⊆ ( Base ‘ 𝐸 ) )
33 2 11 ressbasss ⊢ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐷 )
34 32 33 sstrdi ⊢ ( ( 𝜑 ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ran 𝐹 ⊆ ( Base ‘ 𝐷 ) )
35 28 34 jaodan ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝐷 ) )
36 25 35 ssind ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ran 𝐹 ⊆ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
37 df-f ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) )
38 24 36 37 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → 𝐹 : 𝐴 ⟶ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
39 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
40 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
41 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → 𝑥 ∈ 𝐴 )
42 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → 𝑦 ∈ 𝐴 )
43 1 10 39 40 41 42 funcf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
44 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
45 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 )
46 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝑥 ∈ 𝐴 )
47 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝑦 ∈ 𝐴 )
48 1 10 44 45 46 47 funcf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) )
49 2 39 resshom ⊢ ( 𝑆 ∈ 𝑉 → ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐸 ) )
50 4 49 syl ⊢ ( 𝜑 → ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐸 ) )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐸 ) )
52 51 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) )
53 52 feq3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ) )
54 48 53 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
55 43 54 jaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
56 55 an32s ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
57 38 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
58 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
59 57 58 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
60 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
61 57 60 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
62 59 61 ovresd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( Homf ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
63 59 elin2d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
64 61 elin2d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
65 12 11 39 63 64 homfval ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( Homf ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
66 62 65 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
67 66 feq3d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) )
68 56 67 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ( 𝐹 ‘ 𝑦 ) ) )
69 1 10 16 22 38 68 funcres2b ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Func ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) 𝐺 ) )
70 eqidd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 ) )
71 eqidd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐶 ) )
72 11 ressinbas ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐷 ↾s 𝑆 ) = ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) )
73 4 72 syl ⊢ ( 𝜑 → ( 𝐷 ↾s 𝑆 ) = ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) )
74 2 73 syl5eq ⊢ ( 𝜑 → 𝐸 = ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) )
75 74 fveq2d ⊢ ( 𝜑 → ( Homf ‘ 𝐸 ) = ( Homf ‘ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) )
76 eqid ⊢ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) = ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) )
77 eqid ⊢ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) = ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) )
78 11 12 3 14 76 77 fullresc ⊢ ( 𝜑 → ( ( Homf ‘ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) = ( Homf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) ∧ ( compf ‘ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) = ( compf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) ) )
79 78 simpld ⊢ ( 𝜑 → ( Homf ‘ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) = ( Homf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
80 75 79 eqtrd ⊢ ( 𝜑 → ( Homf ‘ 𝐸 ) = ( Homf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( Homf ‘ 𝐸 ) = ( Homf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
82 74 fveq2d ⊢ ( 𝜑 → ( compf ‘ 𝐸 ) = ( compf ‘ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) )
83 78 simprd ⊢ ( 𝜑 → ( compf ‘ ( 𝐷 ↾s ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) = ( compf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
84 82 83 eqtrd ⊢ ( 𝜑 → ( compf ‘ 𝐸 ) = ( compf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( compf ‘ 𝐸 ) = ( compf ‘ ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
86 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
87 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
88 86 87 sylbi ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
89 88 simpld ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐶 ∈ Cat )
90 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
91 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐸 ) → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
92 90 91 sylbi ⊢ ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
93 92 simpld ⊢ ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 → 𝐶 ∈ Cat )
94 89 93 jaoi ⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝐶 ∈ Cat )
95 94 elexd ⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → 𝐶 ∈ V )
96 95 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → 𝐶 ∈ V )
97 2 ovexi ⊢ 𝐸 ∈ V
98 97 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → 𝐸 ∈ V )
99 ovexd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ∈ V )
100 70 71 81 85 96 96 98 99 funcpropd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( 𝐶 Func 𝐸 ) = ( 𝐶 Func ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) )
101 100 breqd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ↔ 𝐹 ( 𝐶 Func ( 𝐷 ↾cat ( ( Homf ‘ 𝐷 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐷 ) ) ) ) ) ) 𝐺 ) )
102 69 101 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) )
103 102 ex ⊢ ( 𝜑 → ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∨ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) ) )
104 7 9 103 pm5.21ndd ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ) )