Metamath Proof Explorer

Theorem cnelsubclem

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

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

Proof

Step Hyp Ref Expression
1 cnelsubclem.1 ⊢ 𝐽 ∈ V
2 cnelsubclem.2 ⊢ 𝑆 ∈ V
3 cnelsubclem.3 ⊢ ( 𝐶 ∈ Cat ∧ 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) )
4 3 simp1i ⊢ 𝐶 ∈ Cat
5 3 simp2i ⊢ 𝐽 Fn ( 𝑆 × 𝑆 )
6 3 simp3i ⊢ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat )
7 id ⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
8 7 sqxpeqd ⊢ ( 𝑠 = 𝑆 → ( 𝑠 × 𝑠 ) = ( 𝑆 × 𝑆 ) )
9 8 fneq2d ⊢ ( 𝑠 = 𝑆 → ( 𝐽 Fn ( 𝑠 × 𝑠 ) ↔ 𝐽 Fn ( 𝑆 × 𝑆 ) ) )
10 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
11 10 notbid ⊢ ( 𝑠 = 𝑆 → ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
12 11 3anbi2d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) )
13 9 12 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) ↔ ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) ) )
14 2 13 spcev ⊢ ( ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) → ∃ 𝑠 ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) )
15 fneq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 Fn ( 𝑠 × 𝑠 ) ↔ 𝐽 Fn ( 𝑠 × 𝑠 ) ) )
16 breq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ↔ 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ) )
17 oveq ⊢ ( 𝑗 = 𝐽 → ( 𝑥 𝑗 𝑥 ) = ( 𝑥 𝐽 𝑥 ) )
18 17 eleq2d ⊢ ( 𝑗 = 𝐽 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
19 18 ralbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
20 19 notbid ⊢ ( 𝑗 = 𝐽 → ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
21 oveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐶 ↾cat 𝑗 ) = ( 𝐶 ↾cat 𝐽 ) )
22 21 eleq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐶 ↾cat 𝑗 ) ∈ Cat ↔ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) )
23 16 20 22 3anbi123d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) )
24 15 23 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) ↔ ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) ) )
25 24 exbidv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) ↔ ∃ 𝑠 ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) ) )
26 1 25 spcev ⊢ ( ∃ 𝑠 ( 𝐽 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) → ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) )
27 14 26 syl ⊢ ( ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶 ↾cat 𝐽 ) ∈ Cat ) ) → ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) )
28 5 6 27 mp2an ⊢ ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) )
29 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Homf ‘ 𝑐 ) = ( Homf ‘ 𝐶 ) )
30 29 breq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ↔ 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ) )
31 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) )
32 31 fveq1d ⊢ ( 𝑐 = 𝐶 → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
33 32 eleq1d ⊢ ( 𝑐 = 𝐶 → ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ) )
34 33 ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ) )
35 34 notbid ⊢ ( 𝑐 = 𝐶 → ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ) )
36 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ↾cat 𝑗 ) = ( 𝐶 ↾cat 𝑗 ) )
37 36 eleq1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ↾cat 𝑗 ) ∈ Cat ↔ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) )
38 30 35 37 3anbi123d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) ↔ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) )
39 38 anbi2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) ) ↔ ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) ) )
40 39 2exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) ) ↔ ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) ) )
41 40 rspcev ⊢ ( ( 𝐶 ∈ Cat ∧ ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝐶 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝐶 ↾cat 𝑗 ) ∈ Cat ) ) ) → ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) ) )
42 4 28 41 mp2an ⊢ ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) )