Theorem stgredgel

Description: An edge of the star graph S_N. (Contributed by AV, 11-Sep-2025)

	Ref	Expression
Assertion	stgredgel	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝐸 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝐸 = { 0 , 𝑥 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		stgredg	⊢ ( 𝑁 ∈ ℕ0 → ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )
2	1	eleq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ 𝐸 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) )
3		eqeq1	⊢ ( 𝑒 = 𝐸 → ( 𝑒 = { 0 , 𝑥 } ↔ 𝐸 = { 0 , 𝑥 } ) )
4	3	rexbidv	⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ↔ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝐸 = { 0 , 𝑥 } ) )
5	4	elrab	⊢ ( 𝐸 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ↔ ( 𝐸 ∈ 𝒫 ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝐸 = { 0 , 𝑥 } ) )
6		prex	⊢ { 0 , 𝑥 } ∈ V
7		eleq1	⊢ ( 𝐸 = { 0 , 𝑥 } → ( 𝐸 ∈ V ↔ { 0 , 𝑥 } ∈ V ) )
8	6 7	mpbiri	⊢ ( 𝐸 = { 0 , 𝑥 } → 𝐸 ∈ V )
9		elpwg	⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝒫 ( 0 ... 𝑁 ) ↔ 𝐸 ⊆ ( 0 ... 𝑁 ) ) )
10	8 9	syl	⊢ ( 𝐸 = { 0 , 𝑥 } → ( 𝐸 ∈ 𝒫 ( 0 ... 𝑁 ) ↔ 𝐸 ⊆ ( 0 ... 𝑁 ) ) )
11	10	a1i	⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → ( 𝐸 = { 0 , 𝑥 } → ( 𝐸 ∈ 𝒫 ( 0 ... 𝑁 ) ↔ 𝐸 ⊆ ( 0 ... 𝑁 ) ) ) )
12	11	rexlimiv	⊢ ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝐸 = { 0 , 𝑥 } → ( 𝐸 ∈ 𝒫 ( 0 ... 𝑁 ) ↔ 𝐸 ⊆ ( 0 ... 𝑁 ) ) )
13	5 12	bianim	⊢ ( 𝐸 ∈ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ↔ ( 𝐸 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝐸 = { 0 , 𝑥 } ) )
14	2 13	bitrdi	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝐸 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝐸 = { 0 , 𝑥 } ) ) )