Metamath Proof Explorer

Theorem nelsubclem

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

Ref Expression
Hypotheses nelsubc.b 
|- B = ( Base ` C )
nelsubc.s 
|- ( ph -> S C_ B )
nelsubc.0 
|- ( ph -> S =/= (/) )
nelsubc.j 
|- ( ph -> J = ( ( S X. S ) X. { (/) } ) )
nelsubc.h 
|- H = ( Homf ` C )
Assertion nelsubclem 
|- ( ph -> ( J Fn ( S X. S ) /\ ( J C_cat H /\ ( -. A. x e. S I e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) ps ) ) ) )

Proof

Step Hyp Ref Expression
1 nelsubc.b 
 |-  B = ( Base ` C )
2 nelsubc.s 
 |-  ( ph -> S C_ B )
3 nelsubc.0 
 |-  ( ph -> S =/= (/) )
4 nelsubc.j 
 |-  ( ph -> J = ( ( S X. S ) X. { (/) } ) )
5 nelsubc.h 
 |-  H = ( Homf ` C )
6 0ex 
 |-  (/) e. _V
7 fnconstg 
 |-  ( (/) e. _V -> ( ( S X. S ) X. { (/) } ) Fn ( S X. S ) )
8 6 7 ax-mp 
 |-  ( ( S X. S ) X. { (/) } ) Fn ( S X. S )
9 4 fneq1d 
 |-  ( ph -> ( J Fn ( S X. S ) <-> ( ( S X. S ) X. { (/) } ) Fn ( S X. S ) ) )
10 8 9 mpbiri 
 |-  ( ph -> J Fn ( S X. S ) )
11 4 oveqd 
 |-  ( ph -> ( p J q ) = ( p ( ( S X. S ) X. { (/) } ) q ) )
12 6 ovconst2 
 |-  ( ( p e. S /\ q e. S ) -> ( p ( ( S X. S ) X. { (/) } ) q ) = (/) )
13 11 12 sylan9eq 
 |-  ( ( ph /\ ( p e. S /\ q e. S ) ) -> ( p J q ) = (/) )
14 0ss 
 |-  (/) C_ ( p H q )
15 13 14 eqsstrdi 
 |-  ( ( ph /\ ( p e. S /\ q e. S ) ) -> ( p J q ) C_ ( p H q ) )
16 15 ralrimivva 
 |-  ( ph -> A. p e. S A. q e. S ( p J q ) C_ ( p H q ) )
17 5 1 homffn 
 |-  H Fn ( B X. B )
18 17 a1i 
 |-  ( ph -> H Fn ( B X. B ) )
19 1 fvexi 
 |-  B e. _V
20 19 a1i 
 |-  ( ph -> B e. _V )
21 10 18 20 isssc 
 |-  ( ph -> ( J C_cat H <-> ( S C_ B /\ A. p e. S A. q e. S ( p J q ) C_ ( p H q ) ) ) )
22 2 16 21 mpbir2and 
 |-  ( ph -> J C_cat H )
23 4 oveqd 
 |-  ( ph -> ( x J x ) = ( x ( ( S X. S ) X. { (/) } ) x ) )
24 6 ovconst2 
 |-  ( ( x e. S /\ x e. S ) -> ( x ( ( S X. S ) X. { (/) } ) x ) = (/) )
25 24 anidms 
 |-  ( x e. S -> ( x ( ( S X. S ) X. { (/) } ) x ) = (/) )
26 23 25 sylan9eq 
 |-  ( ( ph /\ x e. S ) -> ( x J x ) = (/) )
27 nel02 
 |-  ( ( x J x ) = (/) -> -. I e. ( x J x ) )
28 26 27 syl 
 |-  ( ( ph /\ x e. S ) -> -. I e. ( x J x ) )
29 28 reximdva0 
 |-  ( ( ph /\ S =/= (/) ) -> E. x e. S -. I e. ( x J x ) )
30 3 29 mpdan 
 |-  ( ph -> E. x e. S -. I e. ( x J x ) )
31 rexnal 
 |-  ( E. x e. S -. I e. ( x J x ) <-> -. A. x e. S I e. ( x J x ) )
32 30 31 sylib 
 |-  ( ph -> -. A. x e. S I e. ( x J x ) )
33 4 oveqd 
 |-  ( ph -> ( x J y ) = ( x ( ( S X. S ) X. { (/) } ) y ) )
34 6 ovconst2 
 |-  ( ( x e. S /\ y e. S ) -> ( x ( ( S X. S ) X. { (/) } ) y ) = (/) )
35 33 34 sylan9eq 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x J y ) = (/) )
36 rzal 
 |-  ( ( x J y ) = (/) -> A. f e. ( x J y ) ps )
37 35 36 syl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> A. f e. ( x J y ) ps )
38 37 ralrimivw 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> A. z e. S A. f e. ( x J y ) ps )
39 38 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) ps )
40 32 39 jca 
 |-  ( ph -> ( -. A. x e. S I e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) ps ) )
41 10 22 40 jca32 
 |-  ( ph -> ( J Fn ( S X. S ) /\ ( J C_cat H /\ ( -. A. x e. S I e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) ps ) ) ) )