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 Could not format assertion : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |-

Proof

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