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