Theorem frgrncvvdeqlem1

Description: Lemma 1 for frgrncvvdeq . (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 8-May-2021) (Proof shortened by AV, 12-Feb-2022)

	Ref	Expression
Hypotheses	frgrncvvdeq.v1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrncvvdeq.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	frgrncvvdeq.nx	⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
	frgrncvvdeq.ny	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
	frgrncvvdeq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	frgrncvvdeq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	frgrncvvdeq.ne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
	frgrncvvdeq.xy	⊢ ( 𝜑 → 𝑌 ∉ 𝐷 )
	frgrncvvdeq.f	⊢ ( 𝜑 → 𝐺 ∈ FriendGraph )
	frgrncvvdeq.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
Assertion	frgrncvvdeqlem1	⊢ ( 𝜑 → 𝑋 ∉ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		frgrncvvdeq.v1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrncvvdeq.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		frgrncvvdeq.nx	⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
4		frgrncvvdeq.ny	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
5		frgrncvvdeq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		frgrncvvdeq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		frgrncvvdeq.ne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
8		frgrncvvdeq.xy	⊢ ( 𝜑 → 𝑌 ∉ 𝐷 )
9		frgrncvvdeq.f	⊢ ( 𝜑 → 𝐺 ∈ FriendGraph )
10		frgrncvvdeq.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
11		df-nel	⊢ ( 𝑌 ∉ 𝐷 ↔ ¬ 𝑌 ∈ 𝐷 )
12	3	eleq2i	⊢ ( 𝑌 ∈ 𝐷 ↔ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
13	11 12	xchbinx	⊢ ( 𝑌 ∉ 𝐷 ↔ ¬ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
14	8 13	sylib	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
15		nbgrsym	⊢ ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) ↔ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
16	14 15	sylnibr	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
17		neleq2	⊢ ( 𝑁 = ( 𝐺 NeighbVtx 𝑌 ) → ( 𝑋 ∉ 𝑁 ↔ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑌 ) ) )
18	4 17	ax-mp	⊢ ( 𝑋 ∉ 𝑁 ↔ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑌 ) )
19		df-nel	⊢ ( 𝑋 ∉ ( 𝐺 NeighbVtx 𝑌 ) ↔ ¬ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
20	18 19	bitri	⊢ ( 𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
21	16 20	sylibr	⊢ ( 𝜑 → 𝑋 ∉ 𝑁 )