| Step | Hyp | Ref
| Expression |
| 1 | | frgrncvvdeq.v1 |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | frgrncvvdeq.e |
. . 3
⊢ 𝐸 = (Edg‘𝐺) |
| 3 | | frgrncvvdeq.nx |
. . 3
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) |
| 4 | | frgrncvvdeq.ny |
. . 3
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) |
| 5 | | frgrncvvdeq.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 6 | | frgrncvvdeq.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 7 | | frgrncvvdeq.ne |
. . 3
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
| 8 | | frgrncvvdeq.xy |
. . 3
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
| 9 | | frgrncvvdeq.f |
. . 3
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) |
| 10 | | frgrncvvdeq.a |
. . 3
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | frgrncvvdeqlem4 30321 |
. 2
⊢ (𝜑 → 𝐴:𝐷⟶𝑁) |
| 12 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → 𝐴:𝐷⟶𝑁) |
| 13 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝐴:𝐷⟶𝑁 ∧ 𝑢 ∈ 𝐷) → (𝐴‘𝑢) ∈ 𝑁) |
| 14 | 13 | ad2ant2lr 748 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝐴‘𝑢) ∈ 𝑁) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → (𝐴‘𝑢) ∈ 𝑁) |
| 16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | frgrncvvdeqlem1 30318 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∉ 𝑁) |
| 17 | | preq1 4733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑢 → {𝑥, 𝑦} = {𝑢, 𝑦}) |
| 18 | 17 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑢 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑢, 𝑦} ∈ 𝐸)) |
| 19 | 18 | riotabidv 7390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑢 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = (℩𝑦 ∈ 𝑁 {𝑢, 𝑦} ∈ 𝐸)) |
| 20 | 19 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) = (𝑢 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑢, 𝑦} ∈ 𝐸)) |
| 21 | 10, 20 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐴 = (𝑢 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑢, 𝑦} ∈ 𝐸)) |
| 22 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 21 | frgrncvvdeqlem6 30323 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐷) → {𝑢, (𝐴‘𝑢)} ∈ 𝐸) |
| 23 | | preq1 4733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → {𝑥, 𝑦} = {𝑤, 𝑦}) |
| 24 | 23 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑤, 𝑦} ∈ 𝐸)) |
| 25 | 24 | riotabidv 7390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = (℩𝑦 ∈ 𝑁 {𝑤, 𝑦} ∈ 𝐸)) |
| 26 | 25 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) = (𝑤 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑤, 𝑦} ∈ 𝐸)) |
| 27 | 10, 26 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐴 = (𝑤 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑤, 𝑦} ∈ 𝐸)) |
| 28 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 27 | frgrncvvdeqlem6 30323 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → {𝑤, (𝐴‘𝑤)} ∈ 𝐸) |
| 29 | 22, 28 | anim12dan 619 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸)) |
| 30 | | preq2 4734 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴‘𝑤) = (𝐴‘𝑢) → {𝑤, (𝐴‘𝑤)} = {𝑤, (𝐴‘𝑢)}) |
| 31 | 30 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴‘𝑤) = (𝐴‘𝑢) → ({𝑤, (𝐴‘𝑤)} ∈ 𝐸 ↔ {𝑤, (𝐴‘𝑢)} ∈ 𝐸)) |
| 32 | 31 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴‘𝑤) = (𝐴‘𝑢) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸) ↔ ({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸))) |
| 33 | 32 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴‘𝑢) = (𝐴‘𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸) ↔ ({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸))) |
| 34 | 33 | biimpa 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴‘𝑢) = (𝐴‘𝑤) ∧ ({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸)) → ({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸)) |
| 35 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ≠ 𝑤 ↔ ¬ 𝑢 = 𝑤) |
| 36 | 2, 3 | frgrnbnb 30312 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → (𝐴‘𝑢) = 𝑋)) |
| 37 | 9, 36 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → (𝐴‘𝑢) = 𝑋)) |
| 38 | 37 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → (𝐴‘𝑢) = 𝑋)) |
| 39 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁) |
| 40 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴‘𝑢) = 𝑋 → ((𝐴‘𝑢) ∈ 𝑁 ↔ 𝑋 ∈ 𝑁)) |
| 41 | 40 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐴‘𝑢) = 𝑋 ∧ (𝐴‘𝑢) ∈ 𝑁) → 𝑋 ∈ 𝑁) |
| 42 | 41 | pm2.24d 151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴‘𝑢) = 𝑋 ∧ (𝐴‘𝑢) ∈ 𝑁) → (¬ 𝑋 ∈ 𝑁 → 𝑢 = 𝑤)) |
| 43 | 42 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴‘𝑢) ∈ 𝑁 → ((𝐴‘𝑢) = 𝑋 → (¬ 𝑋 ∈ 𝑁 → 𝑢 = 𝑤))) |
| 44 | 43 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑋 ∈ 𝑁 → ((𝐴‘𝑢) = 𝑋 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
| 45 | 39, 44 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) = 𝑋 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
| 46 | 45 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴‘𝑢) = 𝑋 → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
| 47 | 38, 46 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))) |
| 48 | 47 | expcom 413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ≠ 𝑤 → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
| 49 | 48 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ≠ 𝑤 → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
| 50 | 35, 49 | sylbir 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑢 = 𝑤 → (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ 𝐸) → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
| 51 | 34, 50 | syl5com 31 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑢) = (𝐴‘𝑤) ∧ ({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸)) → (¬ 𝑢 = 𝑤 → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
| 52 | 51 | expcom 413 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 53 | 52 | com24 95 |
. . . . . . . . . . . . . . 15
⊢ (({𝑢, (𝐴‘𝑢)} ∈ 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ 𝐸) → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 54 | 29, 53 | mpcom 38 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
| 55 | 54 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 56 | 55 | com3r 87 |
. . . . . . . . . . . 12
⊢ (¬
𝑢 = 𝑤 → (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 57 | 56 | com15 101 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ 𝑁 → (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 58 | 16, 57 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
| 59 | 58 | expd 415 |
. . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ 𝐷 → (𝑤 ∈ 𝐷 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 60 | 59 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → (𝑢 ∈ 𝐷 → (𝑤 ∈ 𝐷 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
| 61 | 60 | imp42 426 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
| 62 | 15, 61 | mpid 44 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → (¬ 𝑢 = 𝑤 → 𝑢 = 𝑤)) |
| 63 | 62 | pm2.18d 127 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → 𝑢 = 𝑤) |
| 64 | 63 | ex 412 |
. . . 4
⊢ (((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤)) |
| 65 | 64 | ralrimivva 3202 |
. . 3
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → ∀𝑢 ∈ 𝐷 ∀𝑤 ∈ 𝐷 ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤)) |
| 66 | | dff13 7275 |
. . 3
⊢ (𝐴:𝐷–1-1→𝑁 ↔ (𝐴:𝐷⟶𝑁 ∧ ∀𝑢 ∈ 𝐷 ∀𝑤 ∈ 𝐷 ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤))) |
| 67 | 12, 65, 66 | sylanbrc 583 |
. 2
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → 𝐴:𝐷–1-1→𝑁) |
| 68 | 11, 67 | mpdan 687 |
1
⊢ (𝜑 → 𝐴:𝐷–1-1→𝑁) |