Metamath Proof Explorer

Theorem isubgr3stgrlem2

Description: Lemma 2 for isubgr3stgr . (Contributed by AV, 16-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 isubgr3stgrlem2 
|- ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> E. f f : U -1-1-onto-> ( W \ { 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 5 6 stgrorder 
 |-  ( N e. NN0 -> ( # ` W ) = ( N + 1 ) )
8 4 7 ax-mp 
 |-  ( # ` W ) = ( N + 1 )
9 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
10 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
11 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
12 10 11 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
13 4 12 mp1i 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( N + 1 ) - 1 ) = N )
14 9 13 eqtrd 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = N )
15 14 adantr 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( ( # ` W ) - 1 ) = N )
16 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
17 4 16 ax-mp 
 |-  ( N + 1 ) e. NN0
18 eleq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) e. NN0 <-> ( N + 1 ) e. NN0 ) )
19 17 18 mpbiri 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( # ` W ) e. NN0 )
20 19 adantr 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( # ` W ) e. NN0 )
21 6 fvexi 
 |-  W e. _V
22 hashclb 
 |-  ( W e. _V -> ( W e. Fin <-> ( # ` W ) e. NN0 ) )
23 21 22 mp1i 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( W e. Fin <-> ( # ` W ) e. NN0 ) )
24 20 23 mpbird 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> W e. Fin )
25 5 6 stgrvtx0 
 |-  ( N e. NN0 -> 0 e. W )
26 4 25 ax-mp 
 |-  0 e. W
27 hashdifsn 
 |-  ( ( W e. Fin /\ 0 e. W ) -> ( # ` ( W \ { 0 } ) ) = ( ( # ` W ) - 1 ) )
28 24 26 27 sylancl 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( # ` ( W \ { 0 } ) ) = ( ( # ` W ) - 1 ) )
29 simpr3 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( # ` U ) = N )
30 15 28 29 3eqtr4rd 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( # ` U ) = ( # ` ( W \ { 0 } ) ) )
31 eleq1 
 |-  ( ( # ` U ) = N -> ( ( # ` U ) e. NN0 <-> N e. NN0 ) )
32 4 31 mpbiri 
 |-  ( ( # ` U ) = N -> ( # ` U ) e. NN0 )
33 32 3ad2ant3 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( # ` U ) e. NN0 )
34 2 ovexi 
 |-  U e. _V
35 hashclb 
 |-  ( U e. _V -> ( U e. Fin <-> ( # ` U ) e. NN0 ) )
36 34 35 mp1i 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> ( U e. Fin <-> ( # ` U ) e. NN0 ) )
37 33 36 mpbird 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> U e. Fin )
38 diffi 
 |-  ( W e. Fin -> ( W \ { 0 } ) e. Fin )
39 24 38 syl 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( W \ { 0 } ) e. Fin )
40 hasheqf1o 
 |-  ( ( U e. Fin /\ ( W \ { 0 } ) e. Fin ) -> ( ( # ` U ) = ( # ` ( W \ { 0 } ) ) <-> E. f f : U -1-1-onto-> ( W \ { 0 } ) ) )
41 37 39 40 syl2an2 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> ( ( # ` U ) = ( # ` ( W \ { 0 } ) ) <-> E. f f : U -1-1-onto-> ( W \ { 0 } ) ) )
42 30 41 mpbid 
 |-  ( ( ( # ` W ) = ( N + 1 ) /\ ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) ) -> E. f f : U -1-1-onto-> ( W \ { 0 } ) )
43 8 42 mpan 
 |-  ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) -> E. f f : U -1-1-onto-> ( W \ { 0 } ) )