Theorem cnelsubclem 49582

Description: Lemma for cnelsubc 49583. (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 1139	. 2 ⊢ 𝐶 ∈ Cat
3	1	simp2i 1140	. . 3 ⊢ 𝐽 Fn (𝑆 × 𝑆)
4	1	simp3i 1141	. . 3 ⊢ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)
5		cnelsubclem.2	. . . . 5 ⊢ 𝑆 ∈ V
6		id 22	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆)
7	6	sqxpeqd 5672	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
8	7	fneq2d 6614	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝐽 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑆 × 𝑆)))
9		raleq 3298	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
10	9	notbid 318	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
11	10	3anbi2d 1443	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat) ↔ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
12	8, 11	anbi12d 632	. . . . 5 ⊢ (𝑠 = 𝑆 → ((𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) ↔ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
13	5, 12	spcev 3575	. . . 4 ⊢ ((𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
14		cnelsubclem.1	. . . . 5 ⊢ 𝐽 ∈ V
15		fneq1 6611	. . . . . . 7 ⊢ (𝑗 = 𝐽 → (𝑗 Fn (𝑠 × 𝑠) ↔ 𝐽 Fn (𝑠 × 𝑠)))
16		breq1 5112	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (𝑗 ⊆cat (Homf ‘𝐶) ↔ 𝐽 ⊆cat (Homf ‘𝐶)))
17		oveq 7395	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → (𝑥𝑗𝑥) = (𝑥𝐽𝑥))
18	17	eleq2d 2815	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → (((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
19	18	ralbidv 3157	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
20	19	notbid 318	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥)))
21		oveq2 7397	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → (𝐶 ↾cat 𝑗) = (𝐶 ↾cat 𝐽))
22	21	eleq1d 2814	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → ((𝐶 ↾cat 𝑗) ∈ Cat ↔ (𝐶 ↾cat 𝐽) ∈ Cat))
23	16, 20, 22	3anbi123d 1438	. . . . . . 7 ⊢ (𝑗 = 𝐽 → ((𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat) ↔ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)))
24	15, 23	anbi12d 632	. . . . . 6 ⊢ (𝑗 = 𝐽 → ((𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)) ↔ (𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
25	24	exbidv 1921	. . . . 5 ⊢ (𝑗 = 𝐽 → (∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)) ↔ ∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))))
26	14, 25	spcev 3575	. . . 4 ⊢ (∃𝑠(𝐽 Fn (𝑠 × 𝑠) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)))
27	13, 26	syl 17	. . 3 ⊢ ((𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat)) → ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)))
28	3, 4, 27	mp2an 692	. 2 ⊢ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))
29		fveq2 6860	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (Homf ‘𝑐) = (Homf ‘𝐶))
30	29	breq2d 5121	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑗 ⊆cat (Homf ‘𝑐) ↔ 𝑗 ⊆cat (Homf ‘𝐶)))
31		fveq2 6860	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (Id‘𝑐) = (Id‘𝐶))
32	31	fveq1d 6862	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → ((Id‘𝑐)‘𝑥) = ((Id‘𝐶)‘𝑥))
33	32	eleq1d 2814	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
34	33	ralbidv 3157	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
35	34	notbid 318	. . . . . 6 ⊢ (𝑐 = 𝐶 → (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥)))
36		oveq1 7396	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝑐 ↾cat 𝑗) = (𝐶 ↾cat 𝑗))
37	36	eleq1d 2814	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑐 ↾cat 𝑗) ∈ Cat ↔ (𝐶 ↾cat 𝑗) ∈ Cat))
38	30, 35, 37	3anbi123d 1438	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat) ↔ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat)))
39	38	anbi2d 630	. . . 4 ⊢ (𝑐 = 𝐶 → ((𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) ↔ (𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))))
40	39	2exbidv 1924	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)) ↔ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))))
41	40	rspcev 3591	. 2 ⊢ ((𝐶 ∈ Cat ∧ ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝐶 ↾cat 𝑗) ∈ Cat))) → ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat)))
42	2, 28, 41	mp2an 692	1 ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))

Syntax hints:  ¬ wn 3   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  Vcvv 3450   class class class wbr 5109   × cxp 5638   Fn wfn 6508  ‘cfv 6513  (class class class)co 7389  Catccat 17631  Idccid 17632  Hom_f chomf 17633   ⊆_cat cssc 17775   ↾_cat cresc 17776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-iota 6466  df-fun 6515  df-fn 6516  df-fv 6521  df-ov 7392

This theorem is referenced by:  cnelsubc  49583