Metamath Proof Explorer

Theorem cidpropd

Description: Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses catpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
catpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
catpropd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
catpropd.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion cidpropd ( 𝜑 → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 catpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 catpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3 catpropd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 catpropd.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 1 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
7 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10 1 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
11 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
12 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
13 7 8 9 10 11 12 homfeqval ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) )
14 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
15 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
16 1 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
17 2 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
18 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
19 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
20 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
21 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
22 7 8 14 15 16 17 18 19 19 20 21 comfeqval ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) )
23 22 eqeq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
24 13 23 raleqbidva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
25 7 8 9 10 12 11 homfeqval ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
26 10 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
27 2 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
28 12 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
29 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
30 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
31 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
32 7 8 14 15 26 27 28 28 29 30 31 comfeqval ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) )
33 32 eqeq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) )
34 25 33 raleqbidva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) )
35 24 34 anbi12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
36 35 ralbidva ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
37 36 riotabidva ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) = ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
38 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
40 7 8 9 38 39 39 homfeqval ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑥 ) )
41 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
42 41 raleqdv ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
43 40 42 riotaeqbidv ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) = ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
44 37 43 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ Cat ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) = ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
45 6 44 mpteq12dva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
47 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
48 7 8 14 46 47 cidfval ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
49 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
50 1 2 3 4 catpropd ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
51 50 biimpa ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝐷 ∈ Cat )
52 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
53 49 9 15 51 52 cidfval ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( Id ‘ 𝐷 ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐷 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
54 45 48 53 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
55 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ Cat ) → ¬ 𝐶 ∈ Cat )
56 cidffn ⊢ Id Fn Cat
57 56 fndmi ⊢ dom Id = Cat
58 57 eleq2i ⊢ ( 𝐶 ∈ dom Id ↔ 𝐶 ∈ Cat )
59 55 58 sylnibr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ Cat ) → ¬ 𝐶 ∈ dom Id )
60 ndmfv ⊢ ( ¬ 𝐶 ∈ dom Id → ( Id ‘ 𝐶 ) = ∅ )
61 59 60 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ Cat ) → ( Id ‘ 𝐶 ) = ∅ )
62 57 eleq2i ⊢ ( 𝐷 ∈ dom Id ↔ 𝐷 ∈ Cat )
63 50 62 bitr4di ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ dom Id ) )
64 63 notbid ⊢ ( 𝜑 → ( ¬ 𝐶 ∈ Cat ↔ ¬ 𝐷 ∈ dom Id ) )
65 64 biimpa ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ Cat ) → ¬ 𝐷 ∈ dom Id )
66 ndmfv ⊢ ( ¬ 𝐷 ∈ dom Id → ( Id ‘ 𝐷 ) = ∅ )
67 65 66 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ Cat ) → ( Id ‘ 𝐷 ) = ∅ )
68 61 67 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ Cat ) → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
69 54 68 pm2.61dan ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )