Database
GRAPH THEORY
The Friendship Theorem
Huneke's Proof of the Friendship Theorem
frgrncvvdeqlem10
Metamath Proof Explorer
Description: Lemma 10 for frgrncvvdeq . (Contributed by Alexander van der Vekens , 24-Dec-2017) (Revised by AV , 10-May-2021) (Proof shortened by AV , 30-Dec-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
frgrncvvdeqlem10
⊢ ( 𝜑 → 𝐴 : 𝐷 –1-1 -onto → 𝑁 )
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
frgrncvvdeqlem8
⊢ ( 𝜑 → 𝐴 : 𝐷 –1-1 → 𝑁 )
12
1 2 3 4 5 6 7 8 9 10
frgrncvvdeqlem9
⊢ ( 𝜑 → 𝐴 : 𝐷 –onto → 𝑁 )
13
df-f1o
⊢ ( 𝐴 : 𝐷 –1-1 -onto → 𝑁 ↔ ( 𝐴 : 𝐷 –1-1 → 𝑁 ∧ 𝐴 : 𝐷 –onto → 𝑁 ) )
14
11 12 13
sylanbrc
⊢ ( 𝜑 → 𝐴 : 𝐷 –1-1 -onto → 𝑁 )