Metamath Proof Explorer

Theorem catidex

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidex.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
catidex.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
catidex.o ⊢ · = ( comp ‘ 𝐶 )
catidex.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
catidex.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion catidex ( 𝜑 → ∃ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )

Proof

Step Hyp Ref Expression
1 catidex.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 catidex.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 catidex.o ⊢ · = ( comp ‘ 𝐶 )
4 catidex.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 catidex.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7 6 6 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐻 𝑥 ) = ( 𝑋 𝐻 𝑋 ) )
8 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 𝐻 𝑋 ) )
9 opeq2 ⊢ ( 𝑥 = 𝑋 → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑋 ⟩ )
10 9 6 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) = ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) )
11 10 oveqd ⊢ ( 𝑥 = 𝑋 → ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
12 11 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ) )
13 8 12 raleqbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ) )
14 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑦 ) )
15 6 6 opeq12d ⊢ ( 𝑥 = 𝑋 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
16 15 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) = ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) )
17 16 oveqd ⊢ ( 𝑥 = 𝑋 → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) )
18 17 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
19 14 18 raleqbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
20 13 19 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )
21 20 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )
22 7 21 rexeqbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∃ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )
23 1 2 3 iscat ⊢ ( 𝐶 ∈ Cat → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
24 23 ibi ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
25 simpl ⊢ ( ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) → ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
26 25 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
27 4 24 26 3syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
28 22 27 5 rspcdva ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )