Step |
Hyp |
Ref |
Expression |
1 |
|
2pthfrgrrn.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
2pthfrgrrn.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
isfrgr |
⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 ) ) |
4 |
|
reurex |
⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 ) |
5 |
|
prcom |
⊢ { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 } |
6 |
5
|
eleq1i |
⊢ ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { 𝑏 , 𝑎 } ∈ 𝐸 ) |
7 |
6
|
anbi1i |
⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) |
8 |
|
zfpair2 |
⊢ { 𝑏 , 𝑎 } ∈ V |
9 |
|
zfpair2 |
⊢ { 𝑏 , 𝑐 } ∈ V |
10 |
8 9
|
prss |
⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 ) |
11 |
7 10
|
sylbbr |
⊢ ( { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) |
12 |
11
|
reximi |
⊢ ( ∃ 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) |
13 |
4 12
|
syl |
⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) |
14 |
13
|
a1i |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ) → ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) |
15 |
14
|
ralimdvva |
⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) |
16 |
15
|
imp |
⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) |
17 |
3 16
|
sylbi |
⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) |