Metamath Proof Explorer

Theorem cnelsubclem

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

Ref Expression
Hypotheses cnelsubclem.1 
|- J e. _V
cnelsubclem.2 
|- S e. _V
cnelsubclem.3 
|- ( C e. Cat /\ J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) )
Assertion cnelsubclem 
|- E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) )

Proof

Step Hyp Ref Expression
1 cnelsubclem.1 
 |-  J e. _V
2 cnelsubclem.2 
 |-  S e. _V
3 cnelsubclem.3 
 |-  ( C e. Cat /\ J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) )
4 3 simp1i 
 |-  C e. Cat
5 3 simp2i 
 |-  J Fn ( S X. S )
6 3 simp3i 
 |-  ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat )
7 id 
 |-  ( s = S -> s = S )
8 7 sqxpeqd 
 |-  ( s = S -> ( s X. s ) = ( S X. S ) )
9 8 fneq2d 
 |-  ( s = S -> ( J Fn ( s X. s ) <-> J Fn ( S X. S ) ) )
10 raleq 
 |-  ( s = S -> ( A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) <-> A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) ) )
11 10 notbid 
 |-  ( s = S -> ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) <-> -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) ) )
12 11 3anbi2d 
 |-  ( s = S -> ( ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) <-> ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) )
13 9 12 anbi12d 
 |-  ( s = S -> ( ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) <-> ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) ) )
14 2 13 spcev 
 |-  ( ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) -> E. s ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) )
15 fneq1 
 |-  ( j = J -> ( j Fn ( s X. s ) <-> J Fn ( s X. s ) ) )
16 breq1 
 |-  ( j = J -> ( j C_cat ( Homf ` C ) <-> J C_cat ( Homf ` C ) ) )
17 oveq 
 |-  ( j = J -> ( x j x ) = ( x J x ) )
18 17 eleq2d 
 |-  ( j = J -> ( ( ( Id ` C ) ` x ) e. ( x j x ) <-> ( ( Id ` C ) ` x ) e. ( x J x ) ) )
19 18 ralbidv 
 |-  ( j = J -> ( A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) <-> A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) ) )
20 19 notbid 
 |-  ( j = J -> ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) <-> -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) ) )
21 oveq2 
 |-  ( j = J -> ( C |`cat j ) = ( C |`cat J ) )
22 21 eleq1d 
 |-  ( j = J -> ( ( C |`cat j ) e. Cat <-> ( C |`cat J ) e. Cat ) )
23 16 20 22 3anbi123d 
 |-  ( j = J -> ( ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) <-> ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) )
24 15 23 anbi12d 
 |-  ( j = J -> ( ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) <-> ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) ) )
25 24 exbidv 
 |-  ( j = J -> ( E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) <-> E. s ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) ) )
26 1 25 spcev 
 |-  ( E. s ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) -> E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) )
27 14 26 syl 
 |-  ( ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) -> E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) )
28 5 6 27 mp2an 
 |-  E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) )
29 fveq2 
 |-  ( c = C -> ( Homf ` c ) = ( Homf ` C ) )
30 29 breq2d 
 |-  ( c = C -> ( j C_cat ( Homf ` c ) <-> j C_cat ( Homf ` C ) ) )
31 fveq2 
 |-  ( c = C -> ( Id ` c ) = ( Id ` C ) )
32 31 fveq1d 
 |-  ( c = C -> ( ( Id ` c ) ` x ) = ( ( Id ` C ) ` x ) )
33 32 eleq1d 
 |-  ( c = C -> ( ( ( Id ` c ) ` x ) e. ( x j x ) <-> ( ( Id ` C ) ` x ) e. ( x j x ) ) )
34 33 ralbidv 
 |-  ( c = C -> ( A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) <-> A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) ) )
35 34 notbid 
 |-  ( c = C -> ( -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) <-> -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) ) )
36 oveq1 
 |-  ( c = C -> ( c |`cat j ) = ( C |`cat j ) )
37 36 eleq1d 
 |-  ( c = C -> ( ( c |`cat j ) e. Cat <-> ( C |`cat j ) e. Cat ) )
38 30 35 37 3anbi123d 
 |-  ( c = C -> ( ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) <-> ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) )
39 38 anbi2d 
 |-  ( c = C -> ( ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) ) <-> ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) ) )
40 39 2exbidv 
 |-  ( c = C -> ( E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) ) <-> E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) ) )
41 40 rspcev 
 |-  ( ( C e. Cat /\ E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ ( C |`cat j ) e. Cat ) ) ) -> E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) ) )
42 4 28 41 mp2an 
 |-  E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ ( c |`cat j ) e. Cat ) )