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

Proof

Step	Hyp	Ref	Expression
1		fullpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
2		fullpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
3		fullpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
4		fullpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
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 ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
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	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
23		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
24	20 23	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ( 𝐴 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 𝐷 ) )

Metamath Proof Explorer

Theorem fullpropd

Proof