Theorem nelsubc3lem 48931

Description: Lemma for nelsubc3 48932. (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 22	. . . . . . 7 ⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆)
5	4	sqxpeqd 5684	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
6	5	fneq2d 6629	. . . . 5 ⊢ (𝑠 = 𝑆 → (𝐽 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑆 × 𝑆)))
7		raleq 3300	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
8	7	notbid 318	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
9		raleq 3300	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧) ↔ ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
10	9	raleqbi1dv 3315	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧) ↔ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
11	10	raleqbi1dv 3315	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
12	8, 11	anbi12d 632	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) ↔ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))))
13	12	anbi2d 630	. . . . 5 ⊢ (𝑠 = 𝑆 → ((𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))) ↔ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
14	6, 13	anbi12d 632	. . . 4 ⊢ (𝑠 = 𝑆 → ((𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))) ↔ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))))))
15	3, 14	spcev 3583	. . 3 ⊢ ((𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))) → ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
16		nelsubc3lem.j	. . . 4 ⊢ 𝐽 ∈ V
17		fneq1 6626	. . . . . 6 ⊢ (𝑗 = 𝐽 → (𝑗 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑠 × 𝑠)))
18		breq1 5120	. . . . . . 7 ⊢ (𝑗 = 𝐽 → (𝑗 ⊆cat (Homf ‘𝐶) ↔ 𝐽 ⊆cat (Homf ‘𝐶)))
19		oveq 7406	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → (𝑥𝑗𝑥) = (𝑥𝐽𝑥))
20	19	eleq2d 2819	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → (((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
21	20	ralbidv 3161	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
22	21	notbid 318	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
23		oveq 7406	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → (𝑥𝑗𝑦) = (𝑥𝐽𝑦))
24		oveq 7406	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → (𝑦𝑗𝑧) = (𝑦𝐽𝑧))
25		oveq 7406	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐽 → (𝑥𝑗𝑧) = (𝑥𝐽𝑧))
26	25	eleq2d 2819	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
27	24, 26	raleqbidv 3323	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → (∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
28	23, 27	raleqbidv 3323	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
29	28	3ralbidv 3206	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
30	22, 29	anbi12d 632	. . . . . . 7 ⊢ (𝑗 = 𝐽 → ((¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)) ↔ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))))
31	18, 30	anbi12d 632	. . . . . 6 ⊢ (𝑗 = 𝐽 → ((𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) ↔ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
32	17, 31	anbi12d 632	. . . . 5 ⊢ (𝑗 = 𝐽 → ((𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) ↔ (𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))))))
33	32	exbidv 1920	. . . 4 ⊢ (𝑗 = 𝐽 → (∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) ↔ ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))))))
34	16, 33	spcev 3583	. . 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 6873	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (Homf ‘𝑐) = (Homf ‘𝐶))
37	36	breq2d 5129	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑗 ⊆cat (Homf ‘𝑐) ↔ 𝑗 ⊆cat (Homf ‘𝐶)))
38		fveq2 6873	. . . . . . . . . . 11 ⊢ (𝑐 = 𝐶 → (Id‘𝑐) = (Id‘𝐶))
39	38	fveq1d 6875	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ((Id‘𝑐)‘𝑥) = ((Id‘𝐶)‘𝑥))
40	39	eleq1d 2818	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
41	40	ralbidv 3161	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
42	41	notbid 318	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
43		fveq2 6873	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → (comp‘𝑐) = (comp‘𝐶))
44	43	oveqd 7417	. . . . . . . . . . 11 ⊢ (𝑐 = 𝐶 → (⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
45	44	oveqd 7417	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
46	45	eleq1d 2818	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))
47	46	ralbidv 3161	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))
48	47	4ralbidv 3207	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))
49	42, 48	anbi12d 632	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)) ↔ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧))))
50	37, 49	anbi12d 632	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) ↔ (𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))))
51	50	anbi2d 630	. . . 4 ⊢ (𝑐 = 𝐶 → ((𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) ↔ (𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧))))))
52	51	2exbidv 1923	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) ↔ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧))))))
53	52	rspcev 3599	. 2 ⊢ ((𝐶 ∈ Cat ∧ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝑗𝑧))))) → ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))))
54	1, 35, 53	mp2an 692	1 ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))))

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059  Vcvv 3457  ⟨cop 4605   class class class wbr 5117   × cxp 5650   Fn wfn 6523  ‘cfv 6528  (class class class)co 7400  compcco 17270  Catccat 17663  Idccid 17664  Hom_f chomf 17665   ⊆_cat cssc 17807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6530  df-fn 6531  df-fv 6536  df-ov 7403

This theorem is referenced by:  nelsubc3  48932