Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ USGraph) |
2 | | ral0 4441 |
. . . . 5
⊢
∀𝑙 ∈
∅ ∃!𝑥 ∈
{𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
3 | | sneq 4568 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → {𝑘} = {𝑁}) |
4 | 3 | difeq2d 4054 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ({𝑁} ∖ {𝑘}) = ({𝑁} ∖ {𝑁})) |
5 | | difid 4302 |
. . . . . . . 8
⊢ ({𝑁} ∖ {𝑁}) = ∅ |
6 | 4, 5 | eqtrdi 2796 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ({𝑁} ∖ {𝑘}) = ∅) |
7 | | preq2 4667 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑁 → {𝑥, 𝑘} = {𝑥, 𝑁}) |
8 | 7 | preq1d 4672 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝑁}, {𝑥, 𝑙}}) |
9 | 8 | sseq1d 3949 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
10 | 9 | reubidv 3316 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
11 | 6, 10 | raleqbidv 3328 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ∅ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
12 | 11 | ralsng 4606 |
. . . . 5
⊢ (𝑁 ∈ V → (∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ∅ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
13 | 2, 12 | mpbiri 261 |
. . . 4
⊢ (𝑁 ∈ V → ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
14 | | snprc 4650 |
. . . . 5
⊢ (¬
𝑁 ∈ V ↔ {𝑁} = ∅) |
15 | | rzal 4437 |
. . . . 5
⊢ ({𝑁} = ∅ → ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
16 | 14, 15 | sylbi 220 |
. . . 4
⊢ (¬
𝑁 ∈ V →
∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
17 | 13, 16 | pm2.61i 185 |
. . 3
⊢
∀𝑘 ∈
{𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
18 | | id 22 |
. . . . 5
⊢
((Vtx‘𝐺) =
{𝑁} → (Vtx‘𝐺) = {𝑁}) |
19 | | difeq1 4047 |
. . . . . 6
⊢
((Vtx‘𝐺) =
{𝑁} →
((Vtx‘𝐺) ∖
{𝑘}) = ({𝑁} ∖ {𝑘})) |
20 | | reueq1 3336 |
. . . . . 6
⊢
((Vtx‘𝐺) =
{𝑁} → (∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
21 | 19, 20 | raleqbidv 3328 |
. . . . 5
⊢
((Vtx‘𝐺) =
{𝑁} → (∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
22 | 18, 21 | raleqbidv 3328 |
. . . 4
⊢
((Vtx‘𝐺) =
{𝑁} → (∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
23 | 22 | adantl 485 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → (∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
24 | 17, 23 | mpbiri 261 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
25 | | eqid 2739 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
26 | | eqid 2739 |
. . 3
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
27 | 25, 26 | isfrgr 28375 |
. 2
⊢ (𝐺 ∈ FriendGraph ↔
(𝐺 ∈ USGraph ∧
∀𝑘 ∈
(Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
28 | 1, 24, 27 | sylanbrc 586 |
1
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ FriendGraph ) |