Metamath Proof Explorer

Theorem stgr1

Description: The star graph S_1 consists of a single simple edge. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion stgr1 
|- ( StarGr ` 1 ) = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. }

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 stgrfv 
 |-  ( 1 e. NN0 -> ( StarGr ` 1 ) = { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. } )
3 1 2 ax-mp 
 |-  ( StarGr ` 1 ) = { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. }
4 fz01pr 
 |-  ( 0 ... 1 ) = { 0 , 1 }
5 4 opeq2i 
 |-  <. ( Base ` ndx ) , ( 0 ... 1 ) >. = <. ( Base ` ndx ) , { 0 , 1 } >.
6 elsni 
 |-  ( x e. { 1 } -> x = 1 )
7 preq2 
 |-  ( x = 1 -> { 0 , x } = { 0 , 1 } )
8 7 eqeq2d 
 |-  ( x = 1 -> ( e = { 0 , x } <-> e = { 0 , 1 } ) )
9 8 biimpd 
 |-  ( x = 1 -> ( e = { 0 , x } -> e = { 0 , 1 } ) )
10 6 9 syl 
 |-  ( x e. { 1 } -> ( e = { 0 , x } -> e = { 0 , 1 } ) )
11 1z 
 |-  1 e. ZZ
12 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
13 11 12 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
14 10 13 eleq2s 
 |-  ( x e. ( 1 ... 1 ) -> ( e = { 0 , x } -> e = { 0 , 1 } ) )
15 14 rexlimiv 
 |-  ( E. x e. ( 1 ... 1 ) e = { 0 , x } -> e = { 0 , 1 } )
16 15 adantl 
 |-  ( ( e e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) e = { 0 , x } ) -> e = { 0 , 1 } )
17 c0ex 
 |-  0 e. _V
18 17 prid1 
 |-  0 e. { 0 , 1 }
19 18 4 eleqtrri 
 |-  0 e. ( 0 ... 1 )
20 1ex 
 |-  1 e. _V
21 20 prid2 
 |-  1 e. { 0 , 1 }
22 21 4 eleqtrri 
 |-  1 e. ( 0 ... 1 )
23 prelpwi 
 |-  ( ( 0 e. ( 0 ... 1 ) /\ 1 e. ( 0 ... 1 ) ) -> { 0 , 1 } e. ~P ( 0 ... 1 ) )
24 19 22 23 mp2an 
 |-  { 0 , 1 } e. ~P ( 0 ... 1 )
25 eqid 
 |-  { 0 , 1 } = { 0 , 1 }
26 13 rexeqi 
 |-  ( E. x e. ( 1 ... 1 ) { 0 , 1 } = { 0 , x } <-> E. x e. { 1 } { 0 , 1 } = { 0 , x } )
27 7 eqeq2d 
 |-  ( x = 1 -> ( { 0 , 1 } = { 0 , x } <-> { 0 , 1 } = { 0 , 1 } ) )
28 20 27 rexsn 
 |-  ( E. x e. { 1 } { 0 , 1 } = { 0 , x } <-> { 0 , 1 } = { 0 , 1 } )
29 26 28 bitri 
 |-  ( E. x e. ( 1 ... 1 ) { 0 , 1 } = { 0 , x } <-> { 0 , 1 } = { 0 , 1 } )
30 25 29 mpbir 
 |-  E. x e. ( 1 ... 1 ) { 0 , 1 } = { 0 , x }
31 24 30 pm3.2i 
 |-  ( { 0 , 1 } e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) { 0 , 1 } = { 0 , x } )
32 eleq1 
 |-  ( e = { 0 , 1 } -> ( e e. ~P ( 0 ... 1 ) <-> { 0 , 1 } e. ~P ( 0 ... 1 ) ) )
33 eqeq1 
 |-  ( e = { 0 , 1 } -> ( e = { 0 , x } <-> { 0 , 1 } = { 0 , x } ) )
34 33 rexbidv 
 |-  ( e = { 0 , 1 } -> ( E. x e. ( 1 ... 1 ) e = { 0 , x } <-> E. x e. ( 1 ... 1 ) { 0 , 1 } = { 0 , x } ) )
35 32 34 anbi12d 
 |-  ( e = { 0 , 1 } -> ( ( e e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) e = { 0 , x } ) <-> ( { 0 , 1 } e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) { 0 , 1 } = { 0 , x } ) ) )
36 31 35 mpbiri 
 |-  ( e = { 0 , 1 } -> ( e e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) e = { 0 , x } ) )
37 16 36 impbii 
 |-  ( ( e e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) e = { 0 , x } ) <-> e = { 0 , 1 } )
38 37 abbii 
 |-  { e | ( e e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) e = { 0 , x } ) } = { e | e = { 0 , 1 } }
39 df-rab 
 |-  { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } = { e | ( e e. ~P ( 0 ... 1 ) /\ E. x e. ( 1 ... 1 ) e = { 0 , x } ) }
40 df-sn 
 |-  { { 0 , 1 } } = { e | e = { 0 , 1 } }
41 38 39 40 3eqtr4i 
 |-  { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } = { { 0 , 1 } }
42 41 reseq2i 
 |-  ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) = ( _I |` { { 0 , 1 } } )
43 42 opeq2i 
 |-  <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. = <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >.
44 5 43 preq12i 
 |-  { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. } = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. }
45 3 44 eqtri 
 |-  ( StarGr ` 1 ) = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. }