| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ USGraph) |
| 2 | | ral0 4513 |
. . . . 5
⊢
∀𝑙 ∈
∅ ∃!𝑥 ∈
{𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
| 3 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → {𝑘} = {𝑁}) |
| 4 | 3 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ({𝑁} ∖ {𝑘}) = ({𝑁} ∖ {𝑁})) |
| 5 | | difid 4376 |
. . . . . . . 8
⊢ ({𝑁} ∖ {𝑁}) = ∅ |
| 6 | 4, 5 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ({𝑁} ∖ {𝑘}) = ∅) |
| 7 | | preq2 4734 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑁 → {𝑥, 𝑘} = {𝑥, 𝑁}) |
| 8 | 7 | preq1d 4739 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝑁}, {𝑥, 𝑙}}) |
| 9 | 8 | sseq1d 4015 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 10 | 9 | reubidv 3398 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 11 | 6, 10 | raleqbidv 3346 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ∅ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 12 | 11 | ralsng 4675 |
. . . . 5
⊢ (𝑁 ∈ V → (∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ∅ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 13 | 2, 12 | mpbiri 258 |
. . . 4
⊢ (𝑁 ∈ V → ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
| 14 | | snprc 4717 |
. . . . 5
⊢ (¬
𝑁 ∈ V ↔ {𝑁} = ∅) |
| 15 | | rzal 4509 |
. . . . 5
⊢ ({𝑁} = ∅ → ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
| 16 | 14, 15 | sylbi 217 |
. . . 4
⊢ (¬
𝑁 ∈ V →
∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
| 17 | 13, 16 | pm2.61i 182 |
. . 3
⊢
∀𝑘 ∈
{𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
| 18 | | id 22 |
. . . . 5
⊢
((Vtx‘𝐺) =
{𝑁} → (Vtx‘𝐺) = {𝑁}) |
| 19 | | difeq1 4119 |
. . . . . 6
⊢
((Vtx‘𝐺) =
{𝑁} →
((Vtx‘𝐺) ∖
{𝑘}) = ({𝑁} ∖ {𝑘})) |
| 20 | | reueq1 3417 |
. . . . . 6
⊢
((Vtx‘𝐺) =
{𝑁} → (∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 21 | 19, 20 | raleqbidv 3346 |
. . . . 5
⊢
((Vtx‘𝐺) =
{𝑁} → (∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 22 | 18, 21 | raleqbidv 3346 |
. . . 4
⊢
((Vtx‘𝐺) =
{𝑁} → (∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 23 | 22 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → (∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 24 | 17, 23 | mpbiri 258 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
| 25 | | eqid 2737 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 26 | | eqid 2737 |
. . 3
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 27 | 25, 26 | isfrgr 30279 |
. 2
⊢ (𝐺 ∈ FriendGraph ↔
(𝐺 ∈ USGraph ∧
∀𝑘 ∈
(Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
| 28 | 1, 24, 27 | sylanbrc 583 |
1
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ FriendGraph ) |