Theorem frgrncvvdeqlem7

Description: Lemma 7 for frgrncvvdeq . This corresponds to statement 1 in Huneke p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021)

	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	frgrncvvdeqlem7	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 )

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	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { ( 𝐴 ‘ 𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )
12		fvex	⊢ ( 𝐴 ‘ 𝑥 ) ∈ V
13	12	snid	⊢ ( 𝐴 ‘ 𝑥 ) ∈ { ( 𝐴 ‘ 𝑥 ) }
14		eleq2	⊢ ( { ( 𝐴 ‘ 𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) → ( ( 𝐴 ‘ 𝑥 ) ∈ { ( 𝐴 ‘ 𝑥 ) } ↔ ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) ) )
15	14	biimpa	⊢ ( ( { ( 𝐴 ‘ 𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ { ( 𝐴 ‘ 𝑥 ) } ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )
16		elin	⊢ ( ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) ↔ ( ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ 𝑁 ) )
17	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem1	⊢ ( 𝜑 → 𝑋 ∉ 𝑁 )
18		df-nel	⊢ ( 𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁 )
19		nelelne	⊢ ( ¬ 𝑋 ∈ 𝑁 → ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑁 → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
20	18 19	sylbi	⊢ ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑁 → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
21	17 20	syl	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑁 → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑁 → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
23	22	com12	⊢ ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑁 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
24	16 23	simplbiim	⊢ ( ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
25	15 24	syl	⊢ ( ( { ( 𝐴 ‘ 𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ { ( 𝐴 ‘ 𝑥 ) } ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
26	13 25	mpan2	⊢ ( { ( 𝐴 ‘ 𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 ) )
27	11 26	mpcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 )
28	27	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ( 𝐴 ‘ 𝑥 ) ≠ 𝑋 )