Theorem uvtxval

Description: The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 29-Oct-2020) (Revised by AV, 14-Feb-2022)

	Ref	Expression
Hypothesis	uvtxval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	uvtxval	⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }

Proof

Step	Hyp	Ref	Expression
1		uvtxval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		df-uvtx	⊢ UnivVtx = ( 𝑔 ∈ V ↦ { 𝑣 ∈ ( Vtx ‘ 𝑔 ) ∣ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) 𝑛 ∈ ( 𝑔 NeighbVtx 𝑣 ) } )
3		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
4	3 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
5	4	difeq1d	⊢ ( 𝑔 = 𝐺 → ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) = ( 𝑉 ∖ { 𝑣 } ) )
6		oveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 NeighbVtx 𝑣 ) = ( 𝐺 NeighbVtx 𝑣 ) )
7	6	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑛 ∈ ( 𝑔 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
8	5 7	raleqbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) 𝑛 ∈ ( 𝑔 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
9	2 8	fvmptrabfv	⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }
10	1	eqcomi	⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11	10	rabeqi	⊢ { 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) } = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }
12	9 11	eqtri	⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }