This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
fullpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
fullpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
fullpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
fullpropd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fullpropd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
fullpropd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
fullpropd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion fullpropd ( 𝜑 → ( 𝐴 Full 𝐶 ) = ( 𝐵 Full 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fullpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
2 fullpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
3 fullpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
4 fullpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
5 fullpropd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 fullpropd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7 fullpropd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8 fullpropd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9 relfull ⊢ Rel ( 𝐴 Full 𝐶 )
10 relfull ⊢ Rel ( 𝐵 Full 𝐷 )
11 1 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
14 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
16 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
17 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
18 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
19 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 )
20 18 14 19 funcf1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
21 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
22 20 21 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
23 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
24 20 23 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
25 14 15 16 17 22 24 homfeqval ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) )
26 25 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) )
27 13 26 raleqbidva ⊢ ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) )
28 12 27 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) )
29 28 pm5.32da ⊢ ( 𝜑 → ( ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
30 1 2 3 4 5 6 7 8 funcpropd ⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
31 30 breqd ⊢ ( 𝜑 → ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ↔ 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ) )
32 31 anbi1d ⊢ ( 𝜑 → ( ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
33 29 32 bitrd ⊢ ( 𝜑 → ( ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
34 18 15 isfull ⊢ ( 𝑓 ( 𝐴 Full 𝐶 ) 𝑔 ↔ ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ) )
35 eqid ⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
36 35 16 isfull ⊢ ( 𝑓 ( 𝐵 Full 𝐷 ) 𝑔 ↔ ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) )
37 33 34 36 3bitr4g ⊢ ( 𝜑 → ( 𝑓 ( 𝐴 Full 𝐶 ) 𝑔 ↔ 𝑓 ( 𝐵 Full 𝐷 ) 𝑔 ) )
38 9 10 37 eqbrrdiv ⊢ ( 𝜑 → ( 𝐴 Full 𝐶 ) = ( 𝐵 Full 𝐷 ) )