Description: Lemma 4 for frgrncvvdeq . The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-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 | frgrncvvdeqlem4 | ⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑁 ) |
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 | frgrncvvdeqlem2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) |
12 | riotacl | ⊢ ( ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ∈ 𝑁 ) | |
13 | 11 12 | syl | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ∈ 𝑁 ) |
14 | 13 10 | fmptd | ⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑁 ) |