Theorem nelsubc3lem 49907

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

Hypotheses

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

Assertion

Ref	Expression
nelsubc3lem	⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))))

Distinct variable groups:   𝐶,𝑐,𝑓,𝑗,𝑠   𝐶,𝑔,𝑐,𝑗,𝑠   𝑥,𝐶,𝑐,𝑗,𝑠   𝑦,𝐶,𝑐,𝑗,𝑠   𝑧,𝐶,𝑐,𝑗,𝑠   𝑓,𝐽,𝑗,𝑠   𝑔,𝐽   𝑥,𝐽   𝑦,𝐽   𝑧,𝐽   𝑆,𝑠,𝑥   𝑦,𝑆   𝑧,𝑆

Allowed substitution hints:   𝑆(𝑓, 𝑔, 𝑗, 𝑐)   𝐽(𝑐)

Proof of Theorem nelsubc3lem

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091  Vcvv 3457  ⟨cop 4597   class class class wbr 5111   × cxp 5661   Fn wfn 6535  ‘cfv 6540  (class class class)co 7419  compcco 17346  Catccat 17744  Idccid 17745  Hom_f chomf 17746   ⊆_cat cssc 17888

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548  df-ov 7422

This theorem is used by:  nelsubc3  49908