Metamath Proof Explorer

Theorem stgrusgra

Description: The star graph S_N is a simple graph. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion stgrusgra 
|- ( N e. NN0 -> ( StarGr ` N ) e. USGraph )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-onto-> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } }
2 f1of1 
 |-  ( ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-onto-> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )
3 1 2 mp1i 
 |-  ( N e. NN0 -> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )
4 simpllr 
 |-  ( ( ( ( N e. NN0 /\ k e. ~P ( 0 ... N ) ) /\ x e. ( 1 ... N ) ) /\ k = { 0 , x } ) -> k e. ~P ( 0 ... N ) )
5 fveq2 
 |-  ( k = { 0 , x } -> ( # ` k ) = ( # ` { 0 , x } ) )
6 0red 
 |-  ( x e. ( 1 ... N ) -> 0 e. RR )
7 elfznn 
 |-  ( x e. ( 1 ... N ) -> x e. NN )
8 7 nngt0d 
 |-  ( x e. ( 1 ... N ) -> 0 < x )
9 6 8 ltned 
 |-  ( x e. ( 1 ... N ) -> 0 =/= x )
10 c0ex 
 |-  0 e. _V
11 vex 
 |-  x e. _V
12 10 11 pm3.2i 
 |-  ( 0 e. _V /\ x e. _V )
13 hashprg 
 |-  ( ( 0 e. _V /\ x e. _V ) -> ( 0 =/= x <-> ( # ` { 0 , x } ) = 2 ) )
14 12 13 mp1i 
 |-  ( x e. ( 1 ... N ) -> ( 0 =/= x <-> ( # ` { 0 , x } ) = 2 ) )
15 9 14 mpbid 
 |-  ( x e. ( 1 ... N ) -> ( # ` { 0 , x } ) = 2 )
16 15 adantl 
 |-  ( ( ( N e. NN0 /\ k e. ~P ( 0 ... N ) ) /\ x e. ( 1 ... N ) ) -> ( # ` { 0 , x } ) = 2 )
17 5 16 sylan9eqr 
 |-  ( ( ( ( N e. NN0 /\ k e. ~P ( 0 ... N ) ) /\ x e. ( 1 ... N ) ) /\ k = { 0 , x } ) -> ( # ` k ) = 2 )
18 4 17 jca 
 |-  ( ( ( ( N e. NN0 /\ k e. ~P ( 0 ... N ) ) /\ x e. ( 1 ... N ) ) /\ k = { 0 , x } ) -> ( k e. ~P ( 0 ... N ) /\ ( # ` k ) = 2 ) )
19 18 ex 
 |-  ( ( ( N e. NN0 /\ k e. ~P ( 0 ... N ) ) /\ x e. ( 1 ... N ) ) -> ( k = { 0 , x } -> ( k e. ~P ( 0 ... N ) /\ ( # ` k ) = 2 ) ) )
20 19 rexlimdva 
 |-  ( ( N e. NN0 /\ k e. ~P ( 0 ... N ) ) -> ( E. x e. ( 1 ... N ) k = { 0 , x } -> ( k e. ~P ( 0 ... N ) /\ ( # ` k ) = 2 ) ) )
21 20 expimpd 
 |-  ( N e. NN0 -> ( ( k e. ~P ( 0 ... N ) /\ E. x e. ( 1 ... N ) k = { 0 , x } ) -> ( k e. ~P ( 0 ... N ) /\ ( # ` k ) = 2 ) ) )
22 eqeq1 
 |-  ( e = k -> ( e = { 0 , x } <-> k = { 0 , x } ) )
23 22 rexbidv 
 |-  ( e = k -> ( E. x e. ( 1 ... N ) e = { 0 , x } <-> E. x e. ( 1 ... N ) k = { 0 , x } ) )
24 23 elrab 
 |-  ( k e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } <-> ( k e. ~P ( 0 ... N ) /\ E. x e. ( 1 ... N ) k = { 0 , x } ) )
25 fveqeq2 
 |-  ( e = k -> ( ( # ` e ) = 2 <-> ( # ` k ) = 2 ) )
26 25 elrab 
 |-  ( k e. { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } <-> ( k e. ~P ( 0 ... N ) /\ ( # ` k ) = 2 ) )
27 21 24 26 3imtr4g 
 |-  ( N e. NN0 -> ( k e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -> k e. { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) )
28 27 ssrdv 
 |-  ( N e. NN0 -> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } C_ { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } )
29 f1ss 
 |-  ( ( ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } /\ { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } C_ { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) -> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } )
30 3 28 29 syl2anc 
 |-  ( N e. NN0 -> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } )
31 stgriedg 
 |-  ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) )
32 31 dmeqd 
 |-  ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) )
33 dmresi 
 |-  dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } }
34 32 33 eqtrdi 
 |-  ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )
35 stgrvtx 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )
36 35 pweqd 
 |-  ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) )
37 36 rabeqdv 
 |-  ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } )
38 31 34 37 f1eq123d 
 |-  ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) )
39 30 38 mpbird 
 |-  ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } )
40 fvex 
 |-  ( StarGr ` N ) e. _V
41 eqid 
 |-  ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) )
42 eqid 
 |-  ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) )
43 41 42 isusgrs 
 |-  ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) )
44 40 43 mp1i 
 |-  ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) )
45 39 44 mpbird 
 |-  ( N e. NN0 -> ( StarGr ` N ) e. USGraph )