Theorem isuvtx

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

	Ref	Expression
Hypotheses	uvtxel.v	|- V = ( Vtx ` G )
	isuvtx.e	|- E = ( Edg ` G )
Assertion	isuvtx	|- ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e }

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	|- V = ( Vtx ` G )
2		isuvtx.e	|- E = ( Edg ` G )
3	1	uvtxval	|- ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) }
4	1 2	nbgrel	|- ( k e. ( G NeighbVtx v ) <-> ( ( k e. V /\ v e. V ) /\ k =/= v /\ E. e e. E { v , k } C_ e ) )
5		df-3an	|- ( ( ( k e. V /\ v e. V ) /\ k =/= v /\ E. e e. E { v , k } C_ e ) <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) )
6	4 5	bitri	|- ( k e. ( G NeighbVtx v ) <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) )
7		prcom	|- { k , v } = { v , k }
8	7	sseq1i	|- ( { k , v } C_ e <-> { v , k } C_ e )
9	8	rexbii	|- ( E. e e. E { k , v } C_ e <-> E. e e. E { v , k } C_ e )
10		id	|- ( v e. V -> v e. V )
11		eldifi	|- ( k e. ( V \ { v } ) -> k e. V )
12	10 11	anim12ci	|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( k e. V /\ v e. V ) )
13		eldifsni	|- ( k e. ( V \ { v } ) -> k =/= v )
14	13	adantl	|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> k =/= v )
15	12 14	jca	|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( ( k e. V /\ v e. V ) /\ k =/= v ) )
16	15	biantrurd	|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( E. e e. E { v , k } C_ e <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) ) )
17	9 16	syl5rbb	|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) <-> E. e e. E { k , v } C_ e ) )
18	6 17	syl5bb	|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( k e. ( G NeighbVtx v ) <-> E. e e. E { k , v } C_ e ) )
19	18	ralbidva	|- ( v e. V -> ( A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) <-> A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e ) )
20	19	rabbiia	|- { v e. V | A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) } = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e }
21	3 20	eqtri	|- ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e }