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 ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph )

Proof

Step Hyp Ref Expression
1 f1oi ⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1-onto→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } }
2 f1of1 ⊢ ( ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1-onto→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } → ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )
3 1 2 mp1i ⊢ ( 𝑁 ∈ ℕ0 → ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )
4 simpllr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 = { 0 , 𝑥 } ) → 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) )
5 fveq2 ⊢ ( 𝑘 = { 0 , 𝑥 } → ( ♯ ‘ 𝑘 ) = ( ♯ ‘ { 0 , 𝑥 } ) )
6 0red ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 0 ∈ ℝ )
7 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
8 7 nngt0d ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 0 < 𝑥 )
9 6 8 ltned ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 0 ≠ 𝑥 )
10 c0ex ⊢ 0 ∈ V
11 vex ⊢ 𝑥 ∈ V
12 10 11 pm3.2i ⊢ ( 0 ∈ V ∧ 𝑥 ∈ V )
13 hashprg ⊢ ( ( 0 ∈ V ∧ 𝑥 ∈ V ) → ( 0 ≠ 𝑥 ↔ ( ♯ ‘ { 0 , 𝑥 } ) = 2 ) )
14 12 13 mp1i ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → ( 0 ≠ 𝑥 ↔ ( ♯ ‘ { 0 , 𝑥 } ) = 2 ) )
15 9 14 mpbid ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → ( ♯ ‘ { 0 , 𝑥 } ) = 2 )
16 15 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ♯ ‘ { 0 , 𝑥 } ) = 2 )
17 5 16 sylan9eqr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 = { 0 , 𝑥 } ) → ( ♯ ‘ 𝑘 ) = 2 )
18 4 17 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 = { 0 , 𝑥 } ) → ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ( ♯ ‘ 𝑘 ) = 2 ) )
19 18 ex ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 = { 0 , 𝑥 } → ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ( ♯ ‘ 𝑘 ) = 2 ) ) )
20 19 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ) → ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑘 = { 0 , 𝑥 } → ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ( ♯ ‘ 𝑘 ) = 2 ) ) )
21 20 expimpd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑘 = { 0 , 𝑥 } ) → ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ( ♯ ‘ 𝑘 ) = 2 ) ) )
22 eqeq1 ⊢ ( 𝑒 = 𝑘 → ( 𝑒 = { 0 , 𝑥 } ↔ 𝑘 = { 0 , 𝑥 } ) )
23 22 rexbidv ⊢ ( 𝑒 = 𝑘 → ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ↔ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑘 = { 0 , 𝑥 } ) )
24 23 elrab ⊢ ( 𝑘 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ↔ ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑘 = { 0 , 𝑥 } ) )
25 fveqeq2 ⊢ ( 𝑒 = 𝑘 → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ 𝑘 ) = 2 ) )
26 25 elrab ⊢ ( 𝑘 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( 𝑘 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ( ♯ ‘ 𝑘 ) = 2 ) )
27 21 24 26 3imtr4g ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑘 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } → 𝑘 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
28 27 ssrdv ⊢ ( 𝑁 ∈ ℕ0 → { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ⊆ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
29 f1ss ⊢ ( ( ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ∧ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ⊆ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) → ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
30 3 28 29 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
31 stgriedg ⊢ ( 𝑁 ∈ ℕ0 → ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) )
32 31 dmeqd ⊢ ( 𝑁 ∈ ℕ0 → dom ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = dom ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) )
33 dmresi ⊢ dom ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } }
34 32 33 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → dom ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )
35 stgrvtx ⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )
36 35 pweqd ⊢ ( 𝑁 ∈ ℕ0 → 𝒫 ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = 𝒫 ( 0 ... 𝑁 ) )
37 36 rabeqdv ⊢ ( 𝑁 ∈ ℕ0 → { 𝑒 ∈ 𝒫 ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) ∣ ( ♯ ‘ 𝑒 ) = 2 } = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
38 31 34 37 f1eq123d ⊢ ( 𝑁 ∈ ℕ0 → ( ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) : dom ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) : { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } –1-1→ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
39 30 38 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) : dom ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
40 fvex ⊢ ( StarGr ‘ 𝑁 ) ∈ V
41 eqid ⊢ ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
42 eqid ⊢ ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = ( iEdg ‘ ( StarGr ‘ 𝑁 ) )
43 41 42 isusgrs ⊢ ( ( StarGr ‘ 𝑁 ) ∈ V → ( ( StarGr ‘ 𝑁 ) ∈ USGraph ↔ ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) : dom ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
44 40 43 mp1i ⊢ ( 𝑁 ∈ ℕ0 → ( ( StarGr ‘ 𝑁 ) ∈ USGraph ↔ ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) : dom ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
45 39 44 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph )