Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ USGraph ) |
2 | | ral0 4028 |
. . . . 5
⊢
∀𝑙 ∈
∅ ∃!𝑥 ∈
{𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
3 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → {𝑘} = {𝑁}) |
4 | 3 | difeq2d 3690 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ({𝑁} ∖ {𝑘}) = ({𝑁} ∖ {𝑁})) |
5 | | difid 3902 |
. . . . . . . 8
⊢ ({𝑁} ∖ {𝑁}) = ∅ |
6 | 4, 5 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ({𝑁} ∖ {𝑘}) = ∅) |
7 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑁 → {𝑥, 𝑘} = {𝑥, 𝑁}) |
8 | 7 | preq1d 4218 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝑁}, {𝑥, 𝑙}}) |
9 | 8 | sseq1d 3595 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
10 | 9 | reubidv 3103 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
11 | 6, 10 | raleqbidv 3129 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ∅ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
12 | 11 | ralsng 4165 |
. . . . 5
⊢ (𝑁 ∈ V → (∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ∅ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑁}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
13 | 2, 12 | mpbiri 247 |
. . . 4
⊢ (𝑁 ∈ V → ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
14 | | snprc 4197 |
. . . . 5
⊢ (¬
𝑁 ∈ V ↔ {𝑁} = ∅) |
15 | | ral0 4028 |
. . . . . 6
⊢
∀𝑘 ∈
∅ ∀𝑙 ∈
({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
16 | | id 22 |
. . . . . . 7
⊢ ({𝑁} = ∅ → {𝑁} = ∅) |
17 | 16 | raleqdv 3121 |
. . . . . 6
⊢ ({𝑁} = ∅ →
(∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ ∅ ∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
18 | 15, 17 | mpbiri 247 |
. . . . 5
⊢ ({𝑁} = ∅ → ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
19 | 14, 18 | sylbi 206 |
. . . 4
⊢ (¬
𝑁 ∈ V →
∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
20 | 13, 19 | pm2.61i 175 |
. . 3
⊢
∀𝑘 ∈
{𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) |
21 | | id 22 |
. . . . 5
⊢
((Vtx‘𝐺) =
{𝑁} → (Vtx‘𝐺) = {𝑁}) |
22 | | difeq1 3683 |
. . . . . 6
⊢
((Vtx‘𝐺) =
{𝑁} →
((Vtx‘𝐺) ∖
{𝑘}) = ({𝑁} ∖ {𝑘})) |
23 | | reueq1 3117 |
. . . . . 6
⊢
((Vtx‘𝐺) =
{𝑁} → (∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
24 | 22, 23 | raleqbidv 3129 |
. . . . 5
⊢
((Vtx‘𝐺) =
{𝑁} → (∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
25 | 21, 24 | raleqbidv 3129 |
. . . 4
⊢
((Vtx‘𝐺) =
{𝑁} → (∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
26 | 25 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → (∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺) ↔ ∀𝑘 ∈ {𝑁}∀𝑙 ∈ ({𝑁} ∖ {𝑘})∃!𝑥 ∈ {𝑁} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
27 | 20, 26 | mpbiri 247 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)) |
28 | | eqid 2610 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
29 | | eqid 2610 |
. . 3
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
30 | 28, 29 | frgrusgrfrcond 41431 |
. 2
⊢ (𝐺 ∈ FriendGraph ↔
(𝐺 ∈ USGraph ∧
∀𝑘 ∈
(Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
31 | 1, 27, 30 | sylanbrc 695 |
1
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ FriendGraph ) |