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

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 ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )