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 ∈ ℕ0
2 stgrfv ⊢ ( 1 ∈ ℕ0 → ( StarGr ‘ 1 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 1 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
3 1 2 ax-mp ⊢ ( StarGr ‘ 1 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 1 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ }
4 fz01pr ⊢ ( 0 ... 1 ) = { 0 , 1 }
5 4 opeq2i ⊢ ⟨ ( Base ‘ ndx ) , ( 0 ... 1 ) ⟩ = ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩
6 elsni ⊢ ( 𝑥 ∈ { 1 } → 𝑥 = 1 )
7 preq2 ⊢ ( 𝑥 = 1 → { 0 , 𝑥 } = { 0 , 1 } )
8 7 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑒 = { 0 , 𝑥 } ↔ 𝑒 = { 0 , 1 } ) )
9 8 biimpd ⊢ ( 𝑥 = 1 → ( 𝑒 = { 0 , 𝑥 } → 𝑒 = { 0 , 1 } ) )
10 6 9 syl ⊢ ( 𝑥 ∈ { 1 } → ( 𝑒 = { 0 , 𝑥 } → 𝑒 = { 0 , 1 } ) )
11 1z ⊢ 1 ∈ ℤ
12 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
13 11 12 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
14 10 13 eleq2s ⊢ ( 𝑥 ∈ ( 1 ... 1 ) → ( 𝑒 = { 0 , 𝑥 } → 𝑒 = { 0 , 1 } ) )
15 14 rexlimiv ⊢ ( ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } → 𝑒 = { 0 , 1 } )
16 15 adantl ⊢ ( ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ) → 𝑒 = { 0 , 1 } )
17 c0ex ⊢ 0 ∈ V
18 17 prid1 ⊢ 0 ∈ { 0 , 1 }
19 18 4 eleqtrri ⊢ 0 ∈ ( 0 ... 1 )
20 1ex ⊢ 1 ∈ V
21 20 prid2 ⊢ 1 ∈ { 0 , 1 }
22 21 4 eleqtrri ⊢ 1 ∈ ( 0 ... 1 )
23 prelpwi ⊢ ( ( 0 ∈ ( 0 ... 1 ) ∧ 1 ∈ ( 0 ... 1 ) ) → { 0 , 1 } ∈ 𝒫 ( 0 ... 1 ) )
24 19 22 23 mp2an ⊢ { 0 , 1 } ∈ 𝒫 ( 0 ... 1 )
25 eqid ⊢ { 0 , 1 } = { 0 , 1 }
26 13 rexeqi ⊢ ( ∃ 𝑥 ∈ ( 1 ... 1 ) { 0 , 1 } = { 0 , 𝑥 } ↔ ∃ 𝑥 ∈ { 1 } { 0 , 1 } = { 0 , 𝑥 } )
27 7 eqeq2d ⊢ ( 𝑥 = 1 → ( { 0 , 1 } = { 0 , 𝑥 } ↔ { 0 , 1 } = { 0 , 1 } ) )
28 20 27 rexsn ⊢ ( ∃ 𝑥 ∈ { 1 } { 0 , 1 } = { 0 , 𝑥 } ↔ { 0 , 1 } = { 0 , 1 } )
29 26 28 bitri ⊢ ( ∃ 𝑥 ∈ ( 1 ... 1 ) { 0 , 1 } = { 0 , 𝑥 } ↔ { 0 , 1 } = { 0 , 1 } )
30 25 29 mpbir ⊢ ∃ 𝑥 ∈ ( 1 ... 1 ) { 0 , 1 } = { 0 , 𝑥 }
31 24 30 pm3.2i ⊢ ( { 0 , 1 } ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) { 0 , 1 } = { 0 , 𝑥 } )
32 eleq1 ⊢ ( 𝑒 = { 0 , 1 } → ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ↔ { 0 , 1 } ∈ 𝒫 ( 0 ... 1 ) ) )
33 eqeq1 ⊢ ( 𝑒 = { 0 , 1 } → ( 𝑒 = { 0 , 𝑥 } ↔ { 0 , 1 } = { 0 , 𝑥 } ) )
34 33 rexbidv ⊢ ( 𝑒 = { 0 , 1 } → ( ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ↔ ∃ 𝑥 ∈ ( 1 ... 1 ) { 0 , 1 } = { 0 , 𝑥 } ) )
35 32 34 anbi12d ⊢ ( 𝑒 = { 0 , 1 } → ( ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ) ↔ ( { 0 , 1 } ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) { 0 , 1 } = { 0 , 𝑥 } ) ) )
36 31 35 mpbiri ⊢ ( 𝑒 = { 0 , 1 } → ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ) )
37 16 36 impbii ⊢ ( ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ) ↔ 𝑒 = { 0 , 1 } )
38 37 abbii ⊢ { 𝑒 ∣ ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ) } = { 𝑒 ∣ 𝑒 = { 0 , 1 } }
39 df-rab ⊢ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } = { 𝑒 ∣ ( 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∧ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } ) }
40 df-sn ⊢ { { 0 , 1 } } = { 𝑒 ∣ 𝑒 = { 0 , 1 } }
41 38 39 40 3eqtr4i ⊢ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } = { { 0 , 1 } }
42 41 reseq2i ⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } ) = ( I ↾ { { 0 , 1 } } )
43 42 opeq2i ⊢ ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ = ⟨ ( .ef ‘ ndx ) , ( I ↾ { { 0 , 1 } } ) ⟩
44 5 43 preq12i ⊢ { ⟨ ( Base ‘ ndx ) , ( 0 ... 1 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 1 ) ∣ ∃ 𝑥 ∈ ( 1 ... 1 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { { 0 , 1 } } ) ⟩ }
45 3 44 eqtri ⊢ ( StarGr ‘ 1 ) = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { { 0 , 1 } } ) ⟩ }