| Step | Hyp | Ref
| Expression |
| 1 | | frgrncvvdeq.ny |
. . 3
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) |
| 2 | 1 | ineq2i 4217 |
. 2
⊢ ((𝐺 NeighbVtx 𝑥) ∩ 𝑁) = ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) |
| 3 | | frgrncvvdeq.f |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺 ∈ FriendGraph ) |
| 5 | | frgrncvvdeq.nx |
. . . . . . . 8
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) |
| 6 | 5 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) |
| 7 | | frgrncvvdeq.v1 |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
| 8 | 7 | nbgrisvtx 29358 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉) |
| 9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
| 10 | 6, 9 | biimtrid 242 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉)) |
| 11 | 10 | imp 406 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝑉) |
| 12 | | frgrncvvdeq.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ 𝑉) |
| 14 | | frgrncvvdeq.xy |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
| 15 | | elnelne2 3058 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑌 ∉ 𝐷) → 𝑥 ≠ 𝑌) |
| 16 | 14, 15 | sylan2 593 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐷 ∧ 𝜑) → 𝑥 ≠ 𝑌) |
| 17 | 16 | ancoms 458 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 𝑌) |
| 18 | 11, 13, 17 | 3jca 1129 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌)) |
| 19 | | frgrncvvdeq.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
| 20 | 7, 19 | frcond3 30288 |
. . . 4
⊢ (𝐺 ∈ FriendGraph →
((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌) → ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛})) |
| 21 | 4, 18, 20 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛}) |
| 22 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑛 ∈ V |
| 23 | | elinsn 4710 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ V ∧ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛}) → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌))) |
| 24 | 22, 23 | mpan 690 |
. . . . . . . . 9
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌))) |
| 25 | | frgrusgr 30280 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) |
| 26 | 19 | nbusgreledg 29370 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ↔ {𝑛, 𝑥} ∈ 𝐸)) |
| 27 | | prcom 4732 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑛, 𝑥} = {𝑥, 𝑛} |
| 28 | 27 | eleq1i 2832 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑛, 𝑥} ∈ 𝐸 ↔ {𝑥, 𝑛} ∈ 𝐸) |
| 29 | 26, 28 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ↔ {𝑥, 𝑛} ∈ 𝐸)) |
| 30 | 29 | biimpd 229 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸)) |
| 31 | 3, 25, 30 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸)) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸)) |
| 33 | 32 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, 𝑛} ∈ 𝐸)) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, 𝑛} ∈ 𝐸)) |
| 35 | 34 | imp 406 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑥, 𝑛} ∈ 𝐸) |
| 36 | 1 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢ (𝐺 NeighbVtx 𝑌) = 𝑁 |
| 37 | 36 | eleq2i 2833 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑌) ↔ 𝑛 ∈ 𝑁) |
| 38 | 37 | biimpi 216 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑁) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → 𝑛 ∈ 𝑁) |
| 40 | | frgrncvvdeq.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 41 | | frgrncvvdeq.ne |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
| 42 | | frgrncvvdeq.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
| 43 | 7, 19, 5, 1, 40, 12, 41, 14, 3, 42 | frgrncvvdeqlem2 30319 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) |
| 44 | | preq2 4734 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑛 → {𝑥, 𝑦} = {𝑥, 𝑛}) |
| 45 | 44 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑛 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑥, 𝑛} ∈ 𝐸)) |
| 46 | 45 | riota2 7413 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑁 ∧ ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) → ({𝑥, 𝑛} ∈ 𝐸 ↔ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛)) |
| 47 | 39, 43, 46 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ({𝑥, 𝑛} ∈ 𝐸 ↔ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛)) |
| 48 | 35, 47 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛) |
| 49 | 24, 48 | sylan 580 |
. . . . . . . 8
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛) |
| 50 | 49 | eqcomd 2743 |
. . . . . . 7
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → 𝑛 = (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
| 51 | 50 | sneqd 4638 |
. . . . . 6
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}) |
| 52 | | eqeq1 2741 |
. . . . . . 7
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} ↔ {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
| 53 | 52 | adantr 480 |
. . . . . 6
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} ↔ {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
| 54 | 51, 53 | mpbird 257 |
. . . . 5
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}) |
| 55 | 54 | ex 412 |
. . . 4
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
| 56 | 55 | rexlimivw 3151 |
. . 3
⊢
(∃𝑛 ∈
𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
| 57 | 21, 56 | mpcom 38 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}) |
| 58 | 2, 57 | eqtr2id 2790 |
1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁)) |