Step |
Hyp |
Ref |
Expression |
1 |
|
frcond1.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
frcond1.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
frcond1 |
⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) ) |
4 |
|
prex |
⊢ { 𝐴 , 𝑏 } ∈ V |
5 |
|
prex |
⊢ { 𝑏 , 𝐶 } ∈ V |
6 |
4 5
|
prss |
⊢ ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) |
7 |
6
|
bicomi |
⊢ ( { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) |
8 |
7
|
reubii |
⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) |
9 |
3 8
|
syl6ib |
⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) |