Theorem uvtxusgrel

Description: A universal vertex, i.e. an element of the set of all universal vertices, of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

	Ref	Expression
Hypotheses	uvtxnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uvtxusgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	uvtxusgrel	⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uvtxusgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	uvtxusgr	⊢ ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 } )
4	3	eleq2d	⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ 𝑁 ∈ { 𝑣 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 } ) )
5		sneq	⊢ ( 𝑣 = 𝑁 → { 𝑣 } = { 𝑁 } )
6	5	difeq2d	⊢ ( 𝑣 = 𝑁 → ( 𝑉 ∖ { 𝑣 } ) = ( 𝑉 ∖ { 𝑁 } ) )
7		preq2	⊢ ( 𝑣 = 𝑁 → { 𝑘 , 𝑣 } = { 𝑘 , 𝑁 } )
8	7	eleq1d	⊢ ( 𝑣 = 𝑁 → ( { 𝑘 , 𝑣 } ∈ 𝐸 ↔ { 𝑘 , 𝑁 } ∈ 𝐸 ) )
9	6 8	raleqbidv	⊢ ( 𝑣 = 𝑁 → ( ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 ↔ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) )
10	9	elrab	⊢ ( 𝑁 ∈ { 𝑣 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 } ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) )
11	4 10	bitrdi	⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) ) )