Metamath Proof Explorer

Theorem isubgr3stgrlem3

Description: Lemma 3 for isubgr3stgr . (Contributed by AV, 17-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v 
|- V = ( Vtx ` G )
isubgr3stgr.u 
|- U = ( G NeighbVtx X )
isubgr3stgr.c 
|- C = ( G ClNeighbVtx X )
isubgr3stgr.n 
|- N e. NN0
isubgr3stgr.s 
|- S = ( StarGr ` N )
isubgr3stgr.w 
|- W = ( Vtx ` S )
Assertion isubgr3stgrlem3 
|- ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v 
 |-  V = ( Vtx ` G )
2 isubgr3stgr.u 
 |-  U = ( G NeighbVtx X )
3 isubgr3stgr.c 
 |-  C = ( G ClNeighbVtx X )
4 isubgr3stgr.n 
 |-  N e. NN0
5 isubgr3stgr.s 
 |-  S = ( StarGr ` N )
6 isubgr3stgr.w 
 |-  W = ( Vtx ` S )
7 1 2 3 4 5 6 isubgr3stgrlem2 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> E. f f : U -1-1-onto-> ( W \ { 0 } ) )
8 f1odm 
 |-  ( f : U -1-1-onto-> ( W \ { 0 } ) -> dom f = U )
9 simpr 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ f : U -1-1-onto-> ( W \ { 0 } ) ) -> f : U -1-1-onto-> ( W \ { 0 } ) )
10 simpl2 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ f : U -1-1-onto-> ( W \ { 0 } ) ) -> X e. V )
11 c0ex 
 |-  0 e. _V
12 11 a1i 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ f : U -1-1-onto-> ( W \ { 0 } ) ) -> 0 e. _V )
13 neldifsnd 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ f : U -1-1-onto-> ( W \ { 0 } ) ) -> -. 0 e. ( W \ { 0 } ) )
14 df-nel 
 |-  ( 0 e/ ( W \ { 0 } ) <-> -. 0 e. ( W \ { 0 } ) )
15 13 14 sylibr 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ f : U -1-1-onto-> ( W \ { 0 } ) ) -> 0 e/ ( W \ { 0 } ) )
16 eqid 
 |-  ( f u. { <. X , 0 >. } ) = ( f u. { <. X , 0 >. } )
17 1 2 3 16 isubgr3stgrlem1 
 |-  ( ( f : U -1-1-onto-> ( W \ { 0 } ) /\ X e. V /\ ( 0 e. _V /\ 0 e/ ( W \ { 0 } ) ) ) -> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) )
18 9 10 12 15 17 syl112anc 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ f : U -1-1-onto-> ( W \ { 0 } ) ) -> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) )
19 18 ex 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( f : U -1-1-onto-> ( W \ { 0 } ) -> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) ) )
20 f1of 
 |-  ( ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) -> ( f u. { <. X , 0 >. } ) : C --> ( ( W \ { 0 } ) u. { 0 } ) )
21 20 3ad2ant2 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> ( f u. { <. X , 0 >. } ) : C --> ( ( W \ { 0 } ) u. { 0 } ) )
22 3 ovexi 
 |-  C e. _V
23 22 a1i 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> C e. _V )
24 21 23 fexd 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> ( f u. { <. X , 0 >. } ) e. _V )
25 5 6 stgrvtx0 
 |-  ( N e. NN0 -> 0 e. W )
26 4 25 mp1i 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> 0 e. W )
27 26 snssd 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> { 0 } C_ W )
28 undifr 
 |-  ( { 0 } C_ W <-> ( ( W \ { 0 } ) u. { 0 } ) = W )
29 27 28 sylib 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( ( W \ { 0 } ) u. { 0 } ) = W )
30 29 f1oeq3d 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) <-> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> W ) )
31 30 biimpa 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) ) -> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> W )
32 31 3adant3 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> W )
33 simp12 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> X e. V )
34 11 a1i 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> 0 e. _V )
35 nbgrnself2 
 |-  X e/ ( G NeighbVtx X )
36 df-nel 
 |-  ( X e/ ( G NeighbVtx X ) <-> -. X e. ( G NeighbVtx X ) )
37 2 eleq2i 
 |-  ( X e. U <-> X e. ( G NeighbVtx X ) )
38 36 37 xchbinxr 
 |-  ( X e/ ( G NeighbVtx X ) <-> -. X e. U )
39 35 38 mpbi 
 |-  -. X e. U
40 eleq2 
 |-  ( dom f = U -> ( X e. dom f <-> X e. U ) )
41 40 notbid 
 |-  ( dom f = U -> ( -. X e. dom f <-> -. X e. U ) )
42 41 3ad2ant3 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> ( -. X e. dom f <-> -. X e. U ) )
43 39 42 mpbiri 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> -. X e. dom f )
44 fsnunfv 
 |-  ( ( X e. V /\ 0 e. _V /\ -. X e. dom f ) -> ( ( f u. { <. X , 0 >. } ) ` X ) = 0 )
45 33 34 43 44 syl3anc 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> ( ( f u. { <. X , 0 >. } ) ` X ) = 0 )
46 32 45 jca 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> ( ( f u. { <. X , 0 >. } ) : C -1-1-onto-> W /\ ( ( f u. { <. X , 0 >. } ) ` X ) = 0 ) )
47 f1oeq1 
 |-  ( g = ( f u. { <. X , 0 >. } ) -> ( g : C -1-1-onto-> W <-> ( f u. { <. X , 0 >. } ) : C -1-1-onto-> W ) )
48 fveq1 
 |-  ( g = ( f u. { <. X , 0 >. } ) -> ( g ` X ) = ( ( f u. { <. X , 0 >. } ) ` X ) )
49 48 eqeq1d 
 |-  ( g = ( f u. { <. X , 0 >. } ) -> ( ( g ` X ) = 0 <-> ( ( f u. { <. X , 0 >. } ) ` X ) = 0 ) )
50 47 49 anbi12d 
 |-  ( g = ( f u. { <. X , 0 >. } ) -> ( ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) <-> ( ( f u. { <. X , 0 >. } ) : C -1-1-onto-> W /\ ( ( f u. { <. X , 0 >. } ) ` X ) = 0 ) ) )
51 24 46 50 spcedv 
 |-  ( ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) /\ ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) /\ dom f = U ) -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) )
52 51 3exp 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( ( f u. { <. X , 0 >. } ) : C -1-1-onto-> ( ( W \ { 0 } ) u. { 0 } ) -> ( dom f = U -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) ) ) )
53 19 52 syld 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( f : U -1-1-onto-> ( W \ { 0 } ) -> ( dom f = U -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) ) ) )
54 8 53 mpdi 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( f : U -1-1-onto-> ( W \ { 0 } ) -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) ) )
55 54 exlimdv 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( E. f f : U -1-1-onto-> ( W \ { 0 } ) -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) ) )
56 7 55 mpd 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) )