Theorem clnbupgrel

Description: A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025)

	Ref	Expression
Hypotheses	clnbuhgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	clnbuhgr.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	clnbupgrel	Could not format assertion : No typesetting found for |- ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbuhgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		clnbuhgr.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3	1 2	clnbupgr	Could not format ( ( G e. UPGraph /\ K e. V ) -> ( G ClNeighbVtx K ) = ( { K } u. { n e. V | { K , n } e. E } ) ) : No typesetting found for |- ( ( G e. UPGraph /\ K e. V ) -> ( G ClNeighbVtx K ) = ( { K } u. { n e. V | { K , n } e. E } ) ) with typecode |-
4	3	eleq2d	Could not format ( ( G e. UPGraph /\ K e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> N e. ( { K } u. { n e. V | { K , n } e. E } ) ) ) : No typesetting found for |- ( ( G e. UPGraph /\ K e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> N e. ( { K } u. { n e. V | { K , n } e. E } ) ) ) with typecode |-
5	4	3adant3	Could not format ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> N e. ( { K } u. { n e. V | { K , n } e. E } ) ) ) : No typesetting found for |- ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> N e. ( { K } u. { n e. V | { K , n } e. E } ) ) ) with typecode |-
6		elun	$$⊢N\in \left(\left\{K\right\}\cup \left\{n\in V|\left\{K,n\right\}\in E\right\}\right)\leftrightarrow \left(N\in \left\{K\right\}\vee N\in \left\{n\in V|\left\{K,n\right\}\in E\right\}\right)$$
7		preq2	$$⊢n=N\to \left\{K,n\right\}=\left\{K,N\right\}$$
8	7	eleq1d	$$⊢n=N\to \left(\left\{K,n\right\}\in E\leftrightarrow \left\{K,N\right\}\in E\right)$$
9	8	elrab	$$⊢N\in \left\{n\in V|\left\{K,n\right\}\in E\right\}\leftrightarrow \left(N\in V\wedge \left\{K,N\right\}\in E\right)$$
10	9	orbi2i	$$⊢\left(N\in \left\{K\right\}\vee N\in \left\{n\in V|\left\{K,n\right\}\in E\right\}\right)\leftrightarrow \left(N\in \left\{K\right\}\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)$$
11	6 10	bitri	$$⊢N\in \left(\left\{K\right\}\cup \left\{n\in V|\left\{K,n\right\}\in E\right\}\right)\leftrightarrow \left(N\in \left\{K\right\}\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)$$
12		elsng	$$⊢N\in V\to \left(N\in \left\{K\right\}\leftrightarrow N=K\right)$$
13	12	3ad2ant3	$$⊢\left(G\in \mathrm{UPGraph}\wedge K\in V\wedge N\in V\right)\to \left(N\in \left\{K\right\}\leftrightarrow N=K\right)$$
14	13	orbi1d	$$⊢\left(G\in \mathrm{UPGraph}\wedge K\in V\wedge N\in V\right)\to \left(\left(N\in \left\{K\right\}\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)\leftrightarrow \left(N=K\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)\right)$$
15	11 14	bitrid	$$⊢\left(G\in \mathrm{UPGraph}\wedge K\in V\wedge N\in V\right)\to \left(N\in \left(\left\{K\right\}\cup \left\{n\in V|\left\{K,n\right\}\in E\right\}\right)\leftrightarrow \left(N=K\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)\right)$$
16		ibar	$$⊢N\in V\to \left(\left\{K,N\right\}\in E\leftrightarrow \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)$$
17		prcom	$$⊢\left\{K,N\right\}=\left\{N,K\right\}$$
18	17	eleq1i	$$⊢\left\{K,N\right\}\in E\leftrightarrow \left\{N,K\right\}\in E$$
19	16 18	bitr3di	$$⊢N\in V\to \left(\left(N\in V\wedge \left\{K,N\right\}\in E\right)\leftrightarrow \left\{N,K\right\}\in E\right)$$
20	19	orbi2d	$$⊢N\in V\to \left(\left(N=K\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)\leftrightarrow \left(N=K\vee \left\{N,K\right\}\in E\right)\right)$$
21	20	3ad2ant3	$$⊢\left(G\in \mathrm{UPGraph}\wedge K\in V\wedge N\in V\right)\to \left(\left(N=K\vee \left(N\in V\wedge \left\{K,N\right\}\in E\right)\right)\leftrightarrow \left(N=K\vee \left\{N,K\right\}\in E\right)\right)$$
22	5 15 21	3bitrd	Could not format ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) ) : No typesetting found for |- ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) ) with typecode |-