Metamath Proof Explorer

Theorem frgrncvvdeqlem3

Description: Lemma 3 for frgrncvvdeq . The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 10-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 frgrncvvdeqlem3 ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )

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 4 ineq2i ⊢ ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) )
12 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐺 ∈ FriendGraph )
13 3 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
14 1 nbgrisvtx ⊢ ( 𝑥 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑥 ∈ 𝑉 )
15 14 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑥 ∈ 𝑉 ) )
16 13 15 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉 ) )
17 16 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝑉 )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑌 ∈ 𝑉 )
19 elnelne2 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑌 ∉ 𝐷 ) → 𝑥 ≠ 𝑌 )
20 8 19 sylan2 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝜑 ) → 𝑥 ≠ 𝑌 )
21 20 ancoms ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ≠ 𝑌 )
22 17 18 21 3jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌 ) )
23 1 2 frcond3 ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌 ) → ∃ 𝑛 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ) )
24 12 22 23 sylc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑛 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } )
25 vex ⊢ 𝑛 ∈ V
26 elinsn ⊢ ( ( 𝑛 ∈ V ∧ ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) )
27 25 26 mpan ⊢ ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) )
28 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
29 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↔ { 𝑛 , 𝑥 } ∈ 𝐸 ) )
30 prcom ⊢ { 𝑛 , 𝑥 } = { 𝑥 , 𝑛 }
31 30 eleq1i ⊢ ( { 𝑛 , 𝑥 } ∈ 𝐸 ↔ { 𝑥 , 𝑛 } ∈ 𝐸 )
32 29 31 bitrdi ⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↔ { 𝑥 , 𝑛 } ∈ 𝐸 ) )
33 32 biimpd ⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) → { 𝑥 , 𝑛 } ∈ 𝐸 ) )
34 9 28 33 3syl ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) → { 𝑥 , 𝑛 } ∈ 𝐸 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) → { 𝑥 , 𝑛 } ∈ 𝐸 ) )
36 35 com12 ⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { 𝑥 , 𝑛 } ∈ 𝐸 ) )
37 36 adantr ⊢ ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { 𝑥 , 𝑛 } ∈ 𝐸 ) )
38 37 imp ⊢ ( ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → { 𝑥 , 𝑛 } ∈ 𝐸 )
39 4 eqcomi ⊢ ( 𝐺 NeighbVtx 𝑌 ) = 𝑁
40 39 eleq2i ⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ↔ 𝑛 ∈ 𝑁 )
41 40 biimpi ⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) → 𝑛 ∈ 𝑁 )
42 41 adantl ⊢ ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) → 𝑛 ∈ 𝑁 )
43 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 )
44 preq2 ⊢ ( 𝑦 = 𝑛 → { 𝑥 , 𝑦 } = { 𝑥 , 𝑛 } )
45 44 eleq1d ⊢ ( 𝑦 = 𝑛 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑥 , 𝑛 } ∈ 𝐸 ) )
46 45 riota2 ⊢ ( ( 𝑛 ∈ 𝑁 ∧ ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( { 𝑥 , 𝑛 } ∈ 𝐸 ↔ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = 𝑛 ) )
47 42 43 46 syl2an ⊢ ( ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → ( { 𝑥 , 𝑛 } ∈ 𝐸 ↔ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = 𝑛 ) )
48 38 47 mpbid ⊢ ( ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑥 ) ∧ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) ) ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = 𝑛 )
49 27 48 sylan ⊢ ( ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = 𝑛 )
50 49 eqcomd ⊢ ( ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → 𝑛 = ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
51 50 sneqd ⊢ ( ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → { 𝑛 } = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } )
52 eqeq1 ⊢ ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } → ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } ↔ { 𝑛 } = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } ) )
53 52 adantr ⊢ ( ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } ↔ { 𝑛 } = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } ) )
54 51 53 mpbird ⊢ ( ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) → ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } )
55 54 ex ⊢ ( ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } ) )
56 55 rexlimivw ⊢ ( ∃ 𝑛 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { 𝑛 } → ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } ) )
57 24 56 mpcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐺 NeighbVtx 𝑥 ) ∩ ( 𝐺 NeighbVtx 𝑌 ) ) = { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } )
58 11 57 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )