dfsclnbgr6

Description: Alternate definition of a semiclosed neighborhood of a vertex as a union of a semiopen neighborhood and the vertex itself if there is a loop at this vertex. (Contributed by AV, 17-May-2025)

	Ref	Expression
Hypotheses	dfvopnbgr2.v	\|- V = ( Vtx ` G )
	dfvopnbgr2.e	\|- E = ( Edg ` G )
	dfvopnbgr2.u	\|- U = { n e. V \| ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
	dfsclnbgr6.s	\|- S = { n e. V \| E. e e. E { N , n } C_ e }
Assertion	dfsclnbgr6	\|- ( N e. V -> S = ( U u. { n e. { N } \| E. e e. E n e. e } ) )

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	\|- V = ( Vtx ` G )
2		dfvopnbgr2.e	\|- E = ( Edg ` G )
3		dfvopnbgr2.u	\|- U = { n e. V \| ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
4		dfsclnbgr6.s	\|- S = { n e. V \| E. e e. E { N , n } C_ e }
5		simpr	\|- ( ( N e. e /\ n e. e ) -> n e. e )
6	5	anim1i	\|- ( ( ( N e. e /\ n e. e ) /\ n = N ) -> ( n e. e /\ n = N ) )
7	6	olcd	\|- ( ( ( N e. e /\ n e. e ) /\ n = N ) -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) )
8	7	expcom	\|- ( n = N -> ( ( N e. e /\ n e. e ) -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) ) )
9		3anass	\|- ( ( n =/= N /\ N e. e /\ n e. e ) <-> ( n =/= N /\ ( N e. e /\ n e. e ) ) )
10	9	biimpri	\|- ( ( n =/= N /\ ( N e. e /\ n e. e ) ) -> ( n =/= N /\ N e. e /\ n e. e ) )
11	10	orcd	\|- ( ( n =/= N /\ ( N e. e /\ n e. e ) ) -> ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) )
12	11	orcd	\|- ( ( n =/= N /\ ( N e. e /\ n e. e ) ) -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) )
13	12	ex	\|- ( n =/= N -> ( ( N e. e /\ n e. e ) -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) ) )
14	8 13	pm2.61ine	\|- ( ( N e. e /\ n e. e ) -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) )
15		3simpc	\|- ( ( n =/= N /\ N e. e /\ n e. e ) -> ( N e. e /\ n e. e ) )
16	15	a1i	\|- ( N e. V -> ( ( n =/= N /\ N e. e /\ n e. e ) -> ( N e. e /\ n e. e ) ) )
17		vsnid	\|- n e. { n }
18	17	a1i	\|- ( e = { n } -> n e. { n } )
19		eleq2	\|- ( e = { n } -> ( n e. e <-> n e. { n } ) )
20	18 19	mpbird	\|- ( e = { n } -> n e. e )
21	20	adantl	\|- ( ( n = N /\ e = { n } ) -> n e. e )
22		eleq1	\|- ( n = N -> ( n e. e <-> N e. e ) )
23	22	bicomd	\|- ( n = N -> ( N e. e <-> n e. e ) )
24	23	adantr	\|- ( ( n = N /\ e = { n } ) -> ( N e. e <-> n e. e ) )
25	21 24	mpbird	\|- ( ( n = N /\ e = { n } ) -> N e. e )
26	25	adantl	\|- ( ( N e. V /\ ( n = N /\ e = { n } ) ) -> N e. e )
27	21	adantl	\|- ( ( N e. V /\ ( n = N /\ e = { n } ) ) -> n e. e )
28	26 27	jca	\|- ( ( N e. V /\ ( n = N /\ e = { n } ) ) -> ( N e. e /\ n e. e ) )
29	28	ex	\|- ( N e. V -> ( ( n = N /\ e = { n } ) -> ( N e. e /\ n e. e ) ) )
30	16 29	jaod	\|- ( N e. V -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) -> ( N e. e /\ n e. e ) ) )
31	22	biimpac	\|- ( ( n e. e /\ n = N ) -> N e. e )
32		simpl	\|- ( ( n e. e /\ n = N ) -> n e. e )
33	31 32	jca	\|- ( ( n e. e /\ n = N ) -> ( N e. e /\ n e. e ) )
34	33	a1i	\|- ( N e. V -> ( ( n e. e /\ n = N ) -> ( N e. e /\ n e. e ) ) )
35	30 34	jaod	\|- ( N e. V -> ( ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) -> ( N e. e /\ n e. e ) ) )
36	14 35	impbid2	\|- ( N e. V -> ( ( N e. e /\ n e. e ) <-> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) ) )
37	36	rexbidv	\|- ( N e. V -> ( E. e e. E ( N e. e /\ n e. e ) <-> E. e e. E ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) ) )
38		r19.43	\|- ( E. e e. E ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) <-> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ E. e e. E ( n e. e /\ n = N ) ) )
39	38	a1i	\|- ( N e. V -> ( E. e e. E ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n e. e /\ n = N ) ) <-> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ E. e e. E ( n e. e /\ n = N ) ) ) )
40		r19.41v	\|- ( E. e e. E ( n e. e /\ n = N ) <-> ( E. e e. E n e. e /\ n = N ) )
41	40	biancomi	\|- ( E. e e. E ( n e. e /\ n = N ) <-> ( n = N /\ E. e e. E n e. e ) )
42	41	a1i	\|- ( N e. V -> ( E. e e. E ( n e. e /\ n = N ) <-> ( n = N /\ E. e e. E n e. e ) ) )
43	42	orbi2d	\|- ( N e. V -> ( ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ E. e e. E ( n e. e /\ n = N ) ) <-> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n = N /\ E. e e. E n e. e ) ) ) )
44	37 39 43	3bitrd	\|- ( N e. V -> ( E. e e. E ( N e. e /\ n e. e ) <-> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n = N /\ E. e e. E n e. e ) ) ) )
45	44	rabbidv	\|- ( N e. V -> { n e. V \| E. e e. E ( N e. e /\ n e. e ) } = { n e. V \| ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n = N /\ E. e e. E n e. e ) ) } )
46		unrab	\|- ( { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } u. { n e. V \| ( n = N /\ E. e e. E n e. e ) } ) = { n e. V \| ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n = N /\ E. e e. E n e. e ) ) }
47		rabsneq	\|- ( N e. V -> { n e. { N } \| E. e e. E n e. e } = { n e. V \| ( n = N /\ E. e e. E n e. e ) } )
48	47	eqcomd	\|- ( N e. V -> { n e. V \| ( n = N /\ E. e e. E n e. e ) } = { n e. { N } \| E. e e. E n e. e } )
49	48	uneq2d	\|- ( N e. V -> ( { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } u. { n e. V \| ( n = N /\ E. e e. E n e. e ) } ) = ( { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } u. { n e. { N } \| E. e e. E n e. e } ) )
50	46 49	eqtr3id	\|- ( N e. V -> { n e. V \| ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) \/ ( n = N /\ E. e e. E n e. e ) ) } = ( { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } u. { n e. { N } \| E. e e. E n e. e } ) )
51	45 50	eqtrd	\|- ( N e. V -> { n e. V \| E. e e. E ( N e. e /\ n e. e ) } = ( { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } u. { n e. { N } \| E. e e. E n e. e } ) )
52	1 4 2	dfsclnbgr2	\|- ( N e. V -> S = { n e. V \| E. e e. E ( N e. e /\ n e. e ) } )
53	1 2 3	dfvopnbgr2	\|- ( N e. V -> U = { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )
54	53	uneq1d	\|- ( N e. V -> ( U u. { n e. { N } \| E. e e. E n e. e } ) = ( { n e. V \| E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } u. { n e. { N } \| E. e e. E n e. e } ) )
55	51 52 54	3eqtr4d	\|- ( N e. V -> S = ( U u. { n e. { N } \| E. e e. E n e. e } ) )

Metamath Proof Explorer

Theorem dfsclnbgr6

Proof