# Metamath Proof Explorer

## Theorem catideu

Description: Each object in a category has a unique 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 catideu ( 𝜑 → ∃! 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )

### 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 1 2 3 4 5 catidex ( 𝜑 → ∃ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )
7 oveq1 ( 𝑦 = 𝑋 → ( 𝑦 𝐻 𝑋 ) = ( 𝑋 𝐻 𝑋 ) )
8 opeq1 ( 𝑦 = 𝑋 → ⟨ 𝑦 , 𝑋 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
9 8 oveq1d ( 𝑦 = 𝑋 → ( ⟨ 𝑦 , 𝑋· 𝑋 ) = ( ⟨ 𝑋 , 𝑋· 𝑋 ) )
10 9 oveqd ( 𝑦 = 𝑋 → ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) )
11 10 eqeq1d ( 𝑦 = 𝑋 → ( ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ) )
12 7 11 raleqbidv ( 𝑦 = 𝑋 → ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ) )
13 oveq2 ( 𝑦 = 𝑋 → ( 𝑋 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑋 ) )
14 oveq2 ( 𝑦 = 𝑋 → ( ⟨ 𝑋 , 𝑋· 𝑦 ) = ( ⟨ 𝑋 , 𝑋· 𝑋 ) )
15 14 oveqd ( 𝑦 = 𝑋 → ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) )
16 15 eqeq1d ( 𝑦 = 𝑋 → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) )
17 13 16 raleqbidv ( 𝑦 = 𝑋 → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) )
18 12 17 anbi12d ( 𝑦 = 𝑋 → ( ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ) )
19 18 rspcv ( 𝑋𝐵 → ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ) )
20 5 19 syl ( 𝜑 → ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ) )
21 20 ralrimivw ( 𝜑 → ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ) )
22 an3 ( ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ∧ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) )
23 oveq2 ( 𝑓 = → ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) )
24 id ( 𝑓 = 𝑓 = )
25 23 24 eqeq12d ( 𝑓 = → ( ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = ) )
26 25 rspcv ( ∈ ( 𝑋 𝐻 𝑋 ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 → ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = ) )
27 oveq1 ( 𝑓 = 𝑔 → ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) )
28 id ( 𝑓 = 𝑔𝑓 = 𝑔 )
29 27 28 eqeq12d ( 𝑓 = 𝑔 → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑔 ) )
30 29 rspcv ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 → ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑔 ) )
31 26 30 im2anan9r ( ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ ∈ ( 𝑋 𝐻 𝑋 ) ) → ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑔 ) ) )
32 eqtr2 ( ( ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑔 ) → = 𝑔 )
33 32 equcomd ( ( ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑔 ) → 𝑔 = )
34 22 31 33 syl56 ( ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∧ ∈ ( 𝑋 𝐻 𝑋 ) ) → ( ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ∧ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) ) → 𝑔 = ) )
35 34 rgen2 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ ∈ ( 𝑋 𝐻 𝑋 ) ( ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ∧ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) ) → 𝑔 = )
36 35 a1i ( 𝜑 → ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ ∈ ( 𝑋 𝐻 𝑋 ) ( ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ∧ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) ) → 𝑔 = ) )
37 oveq1 ( 𝑔 = → ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) )
38 37 eqeq1d ( 𝑔 = → ( ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ↔ ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ) )
39 38 ralbidv ( 𝑔 = → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ) )
40 oveq2 ( 𝑔 = → ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) )
41 40 eqeq1d ( 𝑔 = → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) )
42 41 ralbidv ( 𝑔 = → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) )
43 39 42 anbi12d ( 𝑔 = → ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) ) )
44 43 rmo4 ( ∃* 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ ∈ ( 𝑋 𝐻 𝑋 ) ( ( ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ∧ ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) ) = 𝑓 ) ) → 𝑔 = ) )
45 36 44 sylibr ( 𝜑 → ∃* 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) )
46 rmoim ( ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) ) → ( ∃* 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑋 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑋 ) 𝑔 ) = 𝑓 ) → ∃* 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
47 21 45 46 sylc ( 𝜑 → ∃* 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )
48 reu5 ( ∃! 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∃ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∃* 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
49 6 47 48 sylanbrc ( 𝜑 → ∃! 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )