Step | Hyp | Ref
| Expression |
1 | | frcond1.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | frcond1.e |
. . 3
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | frgrusgrfrcond 41431 |
. 2
⊢ (𝐺 ∈ FriendGraph ↔
(𝐺 ∈ USGraph ∧
∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑛 ∈ 𝑉 {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸)) |
4 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} ⊆ 𝑉 |
5 | | sseq1 3589 |
. . . . . . . . . . 11
⊢ ({𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥} → ({𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} ⊆ 𝑉 ↔ {𝑥} ⊆ 𝑉)) |
6 | 4, 5 | mpbii 222 |
. . . . . . . . . 10
⊢ ({𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥} → {𝑥} ⊆ 𝑉) |
7 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
8 | 7 | snss 4259 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑉 ↔ {𝑥} ⊆ 𝑉) |
9 | 6, 8 | sylibr 223 |
. . . . . . . . 9
⊢ ({𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥} → 𝑥 ∈ 𝑉) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → 𝑥 ∈ 𝑉) |
11 | 1, 2 | nbusgr 40571 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (𝐺 NeighbVtx 𝑘) = {𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ 𝐸}) |
12 | 1, 2 | nbusgr 40571 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (𝐺 NeighbVtx 𝑙) = {𝑛 ∈ 𝑉 ∣ {𝑙, 𝑛} ∈ 𝐸}) |
13 | 11, 12 | ineq12d 3777 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = ({𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ 𝐸} ∩ {𝑛 ∈ 𝑉 ∣ {𝑙, 𝑛} ∈ 𝐸})) |
14 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) → ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = ({𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ 𝐸} ∩ {𝑛 ∈ 𝑉 ∣ {𝑙, 𝑛} ∈ 𝐸})) |
15 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = ({𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ 𝐸} ∩ {𝑛 ∈ 𝑉 ∣ {𝑙, 𝑛} ∈ 𝐸})) |
16 | | inrab 3858 |
. . . . . . . . . 10
⊢ ({𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ 𝐸} ∩ {𝑛 ∈ 𝑉 ∣ {𝑙, 𝑛} ∈ 𝐸}) = {𝑛 ∈ 𝑉 ∣ ({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸)} |
17 | 15, 16 | syl6eq 2660 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑛 ∈ 𝑉 ∣ ({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸)}) |
18 | | prcom 4211 |
. . . . . . . . . . . . . . 15
⊢ {𝑘, 𝑛} = {𝑛, 𝑘} |
19 | 18 | eleq1i 2679 |
. . . . . . . . . . . . . 14
⊢ ({𝑘, 𝑛} ∈ 𝐸 ↔ {𝑛, 𝑘} ∈ 𝐸) |
20 | | prcom 4211 |
. . . . . . . . . . . . . . 15
⊢ {𝑙, 𝑛} = {𝑛, 𝑙} |
21 | 20 | eleq1i 2679 |
. . . . . . . . . . . . . 14
⊢ ({𝑙, 𝑛} ∈ 𝐸 ↔ {𝑛, 𝑙} ∈ 𝐸) |
22 | 19, 21 | anbi12i 729 |
. . . . . . . . . . . . 13
⊢ (({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸) ↔ ({𝑛, 𝑘} ∈ 𝐸 ∧ {𝑛, 𝑙} ∈ 𝐸)) |
23 | | zfpair2 4834 |
. . . . . . . . . . . . . 14
⊢ {𝑛, 𝑘} ∈ V |
24 | | zfpair2 4834 |
. . . . . . . . . . . . . 14
⊢ {𝑛, 𝑙} ∈ V |
25 | 23, 24 | prss 4291 |
. . . . . . . . . . . . 13
⊢ (({𝑛, 𝑘} ∈ 𝐸 ∧ {𝑛, 𝑙} ∈ 𝐸) ↔ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸) |
26 | 22, 25 | bitri 263 |
. . . . . . . . . . . 12
⊢ (({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸) ↔ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸) |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ 𝑛 ∈ 𝑉) → (({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸) ↔ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸)) |
28 | 27 | rabbidva 3163 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) → {𝑛 ∈ 𝑉 ∣ ({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸)} = {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸}) |
29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → {𝑛 ∈ 𝑉 ∣ ({𝑘, 𝑛} ∈ 𝐸 ∧ {𝑙, 𝑛} ∈ 𝐸)} = {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸}) |
30 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) |
31 | 17, 29, 30 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥}) |
32 | 10, 31 | jca 553 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) ∧ {𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) → (𝑥 ∈ 𝑉 ∧ ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥})) |
33 | 32 | ex 449 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) → ({𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥} → (𝑥 ∈ 𝑉 ∧ ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥}))) |
34 | 33 | eximdv 1833 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) → (∃𝑥{𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥} → ∃𝑥(𝑥 ∈ 𝑉 ∧ ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥}))) |
35 | | reusn 4206 |
. . . . 5
⊢
(∃!𝑛 ∈
𝑉 {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸 ↔ ∃𝑥{𝑛 ∈ 𝑉 ∣ {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸} = {𝑥}) |
36 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑥 ∈
𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥} ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥})) |
37 | 34, 35, 36 | 3imtr4g 284 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ (𝑘 ∈ 𝑉 ∧ 𝑙 ∈ (𝑉 ∖ {𝑘}))) → (∃!𝑛 ∈ 𝑉 {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸 → ∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥})) |
38 | 37 | ralimdvva 2947 |
. . 3
⊢ (𝐺 ∈ USGraph →
(∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑛 ∈ 𝑉 {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸 → ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥})) |
39 | 38 | imp 444 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑛 ∈ 𝑉 {{𝑛, 𝑘}, {𝑛, 𝑙}} ⊆ 𝐸) → ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥}) |
40 | 3, 39 | sylbi 206 |
1
⊢ (𝐺 ∈ FriendGraph →
∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥}) |