Metamath Proof Explorer

Theorem nelsubc3lem

Description: Lemma for nelsubc3 . (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses nelsubc3lem.c ⊢ 𝐶 ∈ Cat
nelsubc3lem.j ⊢ 𝐽 ∈ V
nelsubc3lem.s ⊢ 𝑆 ∈ V
nelsubc3lem.1 ⊢ ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
Assertion nelsubc3lem ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 nelsubc3lem.c ⊢ 𝐶 ∈ Cat
2 nelsubc3lem.j ⊢ 𝐽 ∈ V
3 nelsubc3lem.s ⊢ 𝑆 ∈ V
4 nelsubc3lem.1 ⊢ ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
5 id ⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
6 5 sqxpeqd ⊢ ( 𝑠 = 𝑆 → ( 𝑠 × 𝑠 ) = ( 𝑆 × 𝑆 ) )
7 6 fneq2d ⊢ ( 𝑠 = 𝑆 → ( 𝐽 Fn ( 𝑠 × 𝑠 ) ↔ 𝐽 Fn ( 𝑆 × 𝑆 ) ) )
8 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
9 8 notbid ⊢ ( 𝑠 = 𝑆 → ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
10 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
11 10 raleqbi1dv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
12 11 raleqbi1dv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
13 9 12 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ↔ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
14 13 anbi2d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
15 7 14 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ↔ ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) )
16 3 15 spcev ⊢ ( ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) → ∃ 𝑠 ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
17 fneq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 Fn ( 𝑠 × 𝑠 ) ↔ 𝐽 Fn ( 𝑠 × 𝑠 ) ) )
18 breq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ↔ 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ) )
19 oveq ⊢ ( 𝑗 = 𝐽 → ( 𝑥 𝑗 𝑥 ) = ( 𝑥 𝐽 𝑥 ) )
20 19 eleq2d ⊢ ( 𝑗 = 𝐽 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
21 20 ralbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
22 21 notbid ⊢ ( 𝑗 = 𝐽 → ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
23 oveq ⊢ ( 𝑗 = 𝐽 → ( 𝑥 𝑗 𝑦 ) = ( 𝑥 𝐽 𝑦 ) )
24 oveq ⊢ ( 𝑗 = 𝐽 → ( 𝑦 𝑗 𝑧 ) = ( 𝑦 𝐽 𝑧 ) )
25 oveq ⊢ ( 𝑗 = 𝐽 → ( 𝑥 𝑗 𝑧 ) = ( 𝑥 𝐽 𝑧 ) )
26 25 eleq2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
27 24 26 raleqbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
28 23 27 raleqbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
29 28 3ralbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
30 22 29 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ↔ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
31 18 30 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
32 17 31 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ↔ ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) )
33 32 exbidv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ↔ ∃ 𝑠 ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) )
34 2 33 spcev ⊢ ( ∃ 𝑠 ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) → ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) )
35 4 16 34 mp2b ⊢ ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) )
36 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Homf ‘ 𝑐 ) = ( Homf ‘ 𝐶 ) )
37 36 breq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ↔ 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ) )
38 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) )
39 38 fveq1d ⊢ ( 𝑐 = 𝐶 → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
40 39 eleq1d ⊢ ( 𝑐 = 𝐶 → ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ) )
41 40 ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ) )
42 41 notbid ⊢ ( 𝑐 = 𝐶 → ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ) )
43 fveq2 ⊢ ( 𝑐 = 𝐶 → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
44 43 oveqd ⊢ ( 𝑐 = 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) )
45 44 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
46 45 eleq1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) )
47 46 ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) )
48 47 4ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) )
49 42 48 anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ↔ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) )
50 37 49 anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ↔ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) )
51 50 anbi2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ↔ ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ) )
52 51 2exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ↔ ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ) )
53 52 rspcev ⊢ ( ( 𝐶 ∈ Cat ∧ ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) ) → ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ) )
54 1 35 53 mp2an ⊢ ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) )