Theorem cnelsubcw 50834

Description: A weaker version of cnelsubc 50835, which requires fewer axioms. (Contributed by Zhi Wang, 6-Nov-2025.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem cnelsubcw

Step	Hyp	Ref	Expression
1		cnelsubcw.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		cnelsubcw.2	. . . . 5 ⊢ 𝑆 ∈ V
6		id 23	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆)
7	6	sqxpeqd 5682	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
8	7	fneq2d 6633	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝐽 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑆 × 𝑆)))
9		raleq 3316	. . . . . . . 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 3560	. . . 4 ⊢ ((𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
14		cnelsubcw.1	. . . . 5 ⊢ 𝐽 ∈ V
15		fneq1 6630	. . . . . . 7 ⊢ (𝑗 = 𝐽 → (𝑗 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑠 × 𝑠)))
16		breq1 5105	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (𝑗 ⊆cat (Homf ‘𝐶) ↔ 𝐽 ⊆cat (Homf ‘𝐶)))
17		oveq 7426	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → (𝑥𝑗𝑥) = (𝑥𝐽𝑥))
18	17	eleq2d 2846	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → (((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
19	18	ralbidv 3185	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
20	19	notbid 321	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
21		oveq2 7428	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (𝐶 ↾cat 𝑗) = (𝐶 ↾cat 𝐽))
22	21	eleq1d 2845	. . . . . . . 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 1953	. . . . 5 ⊢ (𝑗 = 𝐽 → (∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)) ↔ ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
26	14, 25	spcev 3560	. . . 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 6885	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (Homf ‘𝑐) = (Homf ‘𝐶))
30	29	breq2d 5114	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑗 ⊆cat (Homf ‘𝑐) ↔ 𝑗 ⊆cat (Homf ‘𝐶)))
31		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (Id‘𝑐) = (Id‘𝐶))
32	31	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → ((Id‘𝑐)‘𝑥) = ((Id‘𝐶)‘𝑥))
33	32	eleq1d 2845	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
34	33	ralbidv 3185	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
35	34	notbid 321	. . . . . 6 ⊢ (𝑐 = 𝐶 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
36		oveq1 7427	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝑐 ↾cat 𝑗) = (𝐶 ↾cat 𝑗))
37	36	eleq1d 2845	. . . . . 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 1956	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) ↔ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))))
41	40	rspcev 3576	. 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 1569  ∃wex 1811   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  Vcvv 3450   class class class wbr 5102   × cxp 5648   Fn wfn 6533  ‘cfv 6538  (class class class)co 7420  Catccat 17843  Idccid 17844  Hom_f chomf 17845   ⊆_cat cssc 17987   ↾_cat cresc 17988

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546  df-ov 7423

This theorem is used by:  cnelsubc  50835