Theorem cnelsubclem 50421

Description: Lemma for cnelsubc 50422. (Contributed by Zhi Wang, 6-Nov-2025.)

Hypotheses

Ref	Expression
cnelsubclem.1	⊢ 𝐽 ∈ V
cnelsubclem.2	⊢ 𝑆 ∈ V
cnelsubclem.3	⊢ (𝐶 ∈ Cat ∧ 𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))

Assertion

Ref	Expression
cnelsubclem	⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))

Distinct variable groups:   𝐶,𝑐,𝑗,𝑠,𝑥   𝑗,𝐽,𝑠,𝑥   𝑆,𝑠,𝑥

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

Proof of Theorem cnelsubclem

Step	Hyp	Ref	Expression
1		cnelsubclem.3	. . 3 ⊢ (𝐶 ∈ Cat ∧ 𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))
2	1	simp1i 1157	. 2 ⊢ 𝐶 ∈ Cat
3	1	simp2i 1158	. . 3 ⊢ 𝐽 Fn (𝑆 × 𝑆)
4	1	simp3i 1159	. . 3 ⊢ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)
5		cnelsubclem.2	. . . . 5 ⊢ 𝑆 ∈ V
6		id 23	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆)
7	6	sqxpeqd 5698	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
8	7	fneq2d 6636	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝐽 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑆 × 𝑆)))
9		raleq 3323	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
10	9	notbid 321	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
11	10	3anbi2d 1469	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat) ↔ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
12	8, 11	anbi12d 644	. . . . 5 ⊢ (𝑠 = 𝑆 → ((𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) ↔ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
13	5, 12	spcev 3568	. . . 4 ⊢ ((𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
14		cnelsubclem.1	. . . . 5 ⊢ 𝐽 ∈ V
15		fneq1 6633	. . . . . . 7 ⊢ (𝑗 = 𝐽 → (𝑗 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑠 × 𝑠)))
16		breq1 5117	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (𝑗 ⊆cat (Homf ‘𝐶) ↔ 𝐽 ⊆cat (Homf ‘𝐶)))
17		oveq 7429	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → (𝑥𝑗𝑥) = (𝑥𝐽𝑥))
18	17	eleq2d 2852	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → (((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
19	18	ralbidv 3191	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
20	19	notbid 321	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
21		oveq2 7431	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (𝐶 ↾cat 𝑗) = (𝐶 ↾cat 𝐽))
22	21	eleq1d 2851	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → ((𝐶 ↾cat 𝑗) ∈ Cat ↔ (𝐶 ↾cat 𝐽) ∈ Cat))
23	16, 20, 22	3anbi123d 1464	. . . . . . 7 ⊢ (𝑗 = 𝐽 → ((𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat) ↔ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
24	15, 23	anbi12d 644	. . . . . 6 ⊢ (𝑗 = 𝐽 → ((𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)) ↔ (𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
25	24	exbidv 1954	. . . . 5 ⊢ (𝑗 = 𝐽 → (∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)) ↔ ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
26	14, 25	spcev 3568	. . . 4 ⊢ (∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)))
27	13, 26	syl 18	. . 3 ⊢ ((𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)))
28	3, 4, 27	mp2an 705	. 2 ⊢ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))
29		fveq2 6888	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (Homf ‘𝑐) = (Homf ‘𝐶))
30	29	breq2d 5126	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑗 ⊆cat (Homf ‘𝑐) ↔ 𝑗 ⊆cat (Homf ‘𝐶)))
31		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (Id‘𝑐) = (Id‘𝐶))
32	31	fveq1d 6890	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → ((Id‘𝑐)‘𝑥) = ((Id‘𝐶)‘𝑥))
33	32	eleq1d 2851	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
34	33	ralbidv 3191	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
35	34	notbid 321	. . . . . 6 ⊢ (𝑐 = 𝐶 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
36		oveq1 7430	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝑐 ↾cat 𝑗) = (𝐶 ↾cat 𝑗))
37	36	eleq1d 2851	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑐 ↾cat 𝑗) ∈ Cat ↔ (𝐶 ↾cat 𝑗) ∈ Cat))
38	30, 35, 37	3anbi123d 1464	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat) ↔ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)))
39	38	anbi2d 642	. . . 4 ⊢ (𝑐 = 𝐶 → ((𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) ↔ (𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))))
40	39	2exbidv 1957	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) ↔ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))))
41	40	rspcev 3584	. 2 ⊢ ((𝐶 ∈ Cat ∧ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))) → ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)))
42	2, 28, 41	mp2an 705	1 ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092  Vcvv 3458   class class class wbr 5114   × cxp 5664   Fn wfn 6538  ‘cfv 6543  (class class class)co 7423  Catccat 17745  Idccid 17746  Hom_f chomf 17747   ⊆_cat cssc 17889   ↾_cat cresc 17890

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 2738

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fn 6546  df-fv 6551  df-ov 7426

This theorem is used by:  cnelsubc  50422