Metamath Proof Explorer

Theorem nelsubc3lem

Description: Lemma for nelsubc3 . (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses nelsubc3lem.c 
|- C e. Cat
nelsubc3lem.j 
|- J e. _V
nelsubc3lem.s 
|- S e. _V
nelsubc3lem.1 
|- ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
Assertion nelsubc3lem 
|- 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) )

Proof

Step Hyp Ref Expression
1 nelsubc3lem.c 
 |-  C e. Cat
2 nelsubc3lem.j 
 |-  J e. _V
3 nelsubc3lem.s 
 |-  S e. _V
4 nelsubc3lem.1 
 |-  ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
5 id 
 |-  ( s = S -> s = S )
6 5 sqxpeqd 
 |-  ( s = S -> ( s X. s ) = ( S X. S ) )
7 6 fneq2d 
 |-  ( s = S -> ( J Fn ( s X. s ) <-> J Fn ( S X. S ) ) )
8 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 ) ) )
9 8 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 ) ) )
10 raleq 
 |-  ( s = S -> ( A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) <-> A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
11 10 raleqbi1dv 
 |-  ( s = S -> ( A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) <-> A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
12 11 raleqbi1dv 
 |-  ( s = S -> ( A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) <-> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
13 9 12 anbi12d 
 |-  ( s = S -> ( ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) <-> ( -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
14 13 anbi2d 
 |-  ( s = S -> ( ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) <-> ( J C_cat ( Homf ` C ) /\ ( -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
15 7 14 anbi12d 
 |-  ( s = S -> ( ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) <-> ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) ) )
16 3 15 spcev 
 |-  ( ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) -> E. s ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
17 fneq1 
 |-  ( j = J -> ( j Fn ( s X. s ) <-> J Fn ( s X. s ) ) )
18 breq1 
 |-  ( j = J -> ( j C_cat ( Homf ` C ) <-> J C_cat ( Homf ` C ) ) )
19 oveq 
 |-  ( j = J -> ( x j x ) = ( x J x ) )
20 19 eleq2d 
 |-  ( j = J -> ( ( ( Id ` C ) ` x ) e. ( x j x ) <-> ( ( Id ` C ) ` x ) e. ( x J x ) ) )
21 20 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 ) ) )
22 21 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 ) ) )
23 oveq 
 |-  ( j = J -> ( x j y ) = ( x J y ) )
24 oveq 
 |-  ( j = J -> ( y j z ) = ( y J z ) )
25 oveq 
 |-  ( j = J -> ( x j z ) = ( x J z ) )
26 25 eleq2d 
 |-  ( j = J -> ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) <-> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
27 24 26 raleqbidv 
 |-  ( j = J -> ( A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) <-> A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
28 23 27 raleqbidv 
 |-  ( j = J -> ( A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) <-> A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
29 28 3ralbidv 
 |-  ( j = J -> ( A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) <-> A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
30 22 29 anbi12d 
 |-  ( j = J -> ( ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) <-> ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
31 18 30 anbi12d 
 |-  ( j = J -> ( ( j C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) <-> ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
32 17 31 anbi12d 
 |-  ( j = J -> ( ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) <-> ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) ) )
33 32 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) <-> E. s ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) ) )
34 2 33 spcev 
 |-  ( E. s ( J Fn ( s X. s ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) -> 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) )
35 4 16 34 mp2b 
 |-  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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) )
36 fveq2 
 |-  ( c = C -> ( Homf ` c ) = ( Homf ` C ) )
37 36 breq2d 
 |-  ( c = C -> ( j C_cat ( Homf ` c ) <-> j C_cat ( Homf ` C ) ) )
38 fveq2 
 |-  ( c = C -> ( Id ` c ) = ( Id ` C ) )
39 38 fveq1d 
 |-  ( c = C -> ( ( Id ` c ) ` x ) = ( ( Id ` C ) ` x ) )
40 39 eleq1d 
 |-  ( c = C -> ( ( ( Id ` c ) ` x ) e. ( x j x ) <-> ( ( Id ` C ) ` x ) e. ( x j x ) ) )
41 40 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 ) ) )
42 41 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 ) ) )
43 fveq2 
 |-  ( c = C -> ( comp ` c ) = ( comp ` C ) )
44 43 oveqd 
 |-  ( c = C -> ( <. x , y >. ( comp ` c ) z ) = ( <. x , y >. ( comp ` C ) z ) )
45 44 oveqd 
 |-  ( c = C -> ( g ( <. x , y >. ( comp ` c ) z ) f ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) )
46 45 eleq1d 
 |-  ( c = C -> ( ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) <-> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) )
47 46 ralbidv 
 |-  ( c = C -> ( A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) <-> A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) )
48 47 4ralbidv 
 |-  ( c = C -> ( A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) <-> A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) )
49 42 48 anbi12d 
 |-  ( c = C -> ( ( -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) <-> ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) )
50 37 49 anbi12d 
 |-  ( c = C -> ( ( j C_cat ( Homf ` c ) /\ ( -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) <-> ( j C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) )
51 50 anbi2d 
 |-  ( c = C -> ( ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ ( -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) ) <-> ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` C ) /\ ( -. A. x e. s ( ( Id ` C ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) ) )
52 51 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) ) <-> 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) ) )
53 52 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x j z ) ) ) ) ) -> 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) ) )
54 1 35 53 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 ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) )