Step | Hyp | Ref
| Expression |
1 | | frgrancvvdeq.nx |
. . 3
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) |
2 | | frgrancvvdeq.ny |
. . 3
⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) |
3 | | frgrancvvdeq.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
4 | | frgrancvvdeq.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
5 | | frgrancvvdeq.ne |
. . 3
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
6 | | frgrancvvdeq.xy |
. . 3
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
7 | | frgrancvvdeq.f |
. . 3
⊢ (𝜑 → 𝑉 FriendGrph 𝐸) |
8 | | frgrancvvdeq.a |
. . 3
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | frgrancvvdeqlem5 26561 |
. 2
⊢ (𝜑 → 𝐴:𝐷⟶𝑁) |
10 | | ffn 5958 |
. . . . . 6
⊢ (𝐴:𝐷⟶𝑁 → 𝐴 Fn 𝐷) |
11 | | dffn3 5967 |
. . . . . 6
⊢ (𝐴 Fn 𝐷 ↔ 𝐴:𝐷⟶ran 𝐴) |
12 | 10, 11 | sylib 207 |
. . . . 5
⊢ (𝐴:𝐷⟶𝑁 → 𝐴:𝐷⟶ran 𝐴) |
13 | 12 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → 𝐴:𝐷⟶ran 𝐴) |
14 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐴:𝐷⟶𝑁 ∧ 𝑢 ∈ 𝐷) → (𝐴‘𝑢) ∈ 𝑁) |
15 | 14 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) → (𝐴‘𝑢) ∈ 𝑁) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) ∧ 𝑤 ∈ 𝐷) → (𝐴‘𝑢) ∈ 𝑁) |
17 | 16 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) ∧ 𝑤 ∈ 𝐷) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → (𝐴‘𝑢) ∈ 𝑁) |
18 | 1, 2, 3, 4, 5, 6, 7, 8 | frgrancvvdeqlem2 26558 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∉ 𝑁) |
19 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑢 → {𝑥, 𝑦} = {𝑢, 𝑦}) |
20 | 19 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑢 → ({𝑥, 𝑦} ∈ ran 𝐸 ↔ {𝑢, 𝑦} ∈ ran 𝐸)) |
21 | 20 | riotabidv 6513 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑢 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸) = (℩𝑦 ∈ 𝑁 {𝑢, 𝑦} ∈ ran 𝐸)) |
22 | 21 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) = (𝑢 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑢, 𝑦} ∈ ran 𝐸)) |
23 | 8, 22 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐴 = (𝑢 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑢, 𝑦} ∈ ran 𝐸)) |
24 | 1, 2, 3, 4, 5, 6, 7, 23 | frgrancvvdeqlem7 26563 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐷) → {𝑢, (𝐴‘𝑢)} ∈ ran 𝐸) |
25 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → {𝑥, 𝑦} = {𝑤, 𝑦}) |
26 | 25 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → ({𝑥, 𝑦} ∈ ran 𝐸 ↔ {𝑤, 𝑦} ∈ ran 𝐸)) |
27 | 26 | riotabidv 6513 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸) = (℩𝑦 ∈ 𝑁 {𝑤, 𝑦} ∈ ran 𝐸)) |
28 | 27 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) = (𝑤 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑤, 𝑦} ∈ ran 𝐸)) |
29 | 8, 28 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐴 = (𝑤 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑤, 𝑦} ∈ ran 𝐸)) |
30 | 1, 2, 3, 4, 5, 6, 7, 29 | frgrancvvdeqlem7 26563 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸) |
31 | 24, 30 | anim12dan 878 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸)) |
32 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴‘𝑤) = (𝐴‘𝑢) → {𝑤, (𝐴‘𝑤)} = {𝑤, (𝐴‘𝑢)}) |
33 | 32 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴‘𝑤) = (𝐴‘𝑢) → ({𝑤, (𝐴‘𝑤)} ∈ ran 𝐸 ↔ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸)) |
34 | 33 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴‘𝑤) = (𝐴‘𝑢) → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸) ↔ ({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸))) |
35 | 34 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴‘𝑢) = (𝐴‘𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸) ↔ ({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸))) |
36 | 35 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴‘𝑢) = (𝐴‘𝑤) ∧ ({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸)) → ({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸)) |
37 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ≠ 𝑤 ↔ ¬ 𝑢 = 𝑤) |
38 | 3, 1, 7 | frgranbnb 26547 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸) → (𝐴‘𝑢) = 𝑋)) |
39 | 38 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸) → (𝐴‘𝑢) = 𝑋)) |
40 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁) |
41 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴‘𝑢) = 𝑋 → ((𝐴‘𝑢) ∈ 𝑁 ↔ 𝑋 ∈ 𝑁)) |
42 | 41 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐴‘𝑢) = 𝑋 ∧ (𝐴‘𝑢) ∈ 𝑁) → 𝑋 ∈ 𝑁) |
43 | 42 | pm2.24d 146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐴‘𝑢) = 𝑋 ∧ (𝐴‘𝑢) ∈ 𝑁) → (¬ 𝑋 ∈ 𝑁 → 𝑢 = 𝑤)) |
44 | 43 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴‘𝑢) ∈ 𝑁 → ((𝐴‘𝑢) = 𝑋 → (¬ 𝑋 ∈ 𝑁 → 𝑢 = 𝑤))) |
45 | 44 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑋 ∈ 𝑁 → ((𝐴‘𝑢) = 𝑋 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
46 | 40, 45 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) = 𝑋 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴‘𝑢) = 𝑋 → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
48 | 39, 47 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑢 ≠ 𝑤) → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))) |
49 | 48 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ≠ 𝑤 → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
50 | 49 | com23 84 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ≠ 𝑤 → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸) → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
51 | 37, 50 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑢 = 𝑤 → (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑢)} ∈ ran 𝐸) → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
52 | 36, 51 | syl5com 31 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴‘𝑢) = (𝐴‘𝑤) ∧ ({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸)) → (¬ 𝑢 = 𝑤 → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
53 | 52 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
54 | 53 | com24 93 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑢, (𝐴‘𝑢)} ∈ ran 𝐸 ∧ {𝑤, (𝐴‘𝑤)} ∈ ran 𝐸) → ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
55 | 31, 54 | mpcom 37 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
56 | 55 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
57 | 56 | com3r 85 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑢 = 𝑤 → (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (𝑋 ∉ 𝑁 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
58 | 57 | com15 99 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∉ 𝑁 → (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
59 | 18, 58 | mpcom 37 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))))) |
60 | 59 | expd 451 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ 𝐷 → (𝑤 ∈ 𝐷 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → (𝑢 ∈ 𝐷 → (𝑤 ∈ 𝐷 → ((𝐴‘𝑢) = (𝐴‘𝑤) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤)))))) |
62 | 61 | imp41 617 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) ∧ 𝑤 ∈ 𝐷) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → (¬ 𝑢 = 𝑤 → ((𝐴‘𝑢) ∈ 𝑁 → 𝑢 = 𝑤))) |
63 | 17, 62 | mpid 43 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) ∧ 𝑤 ∈ 𝐷) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → (¬ 𝑢 = 𝑤 → 𝑢 = 𝑤)) |
64 | 63 | pm2.18d 123 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) ∧ 𝑤 ∈ 𝐷) ∧ (𝐴‘𝑢) = (𝐴‘𝑤)) → 𝑢 = 𝑤) |
65 | 64 | ex 449 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) ∧ 𝑤 ∈ 𝐷) → ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤)) |
66 | 65 | ralrimiva 2949 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴:𝐷⟶𝑁) ∧ 𝑢 ∈ 𝐷) → ∀𝑤 ∈ 𝐷 ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤)) |
67 | 66 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → ∀𝑢 ∈ 𝐷 ∀𝑤 ∈ 𝐷 ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤)) |
68 | | dff13 6416 |
. . . 4
⊢ (𝐴:𝐷–1-1→ran 𝐴 ↔ (𝐴:𝐷⟶ran 𝐴 ∧ ∀𝑢 ∈ 𝐷 ∀𝑤 ∈ 𝐷 ((𝐴‘𝑢) = (𝐴‘𝑤) → 𝑢 = 𝑤))) |
69 | 13, 67, 68 | sylanbrc 695 |
. . 3
⊢ ((𝜑 ∧ 𝐴:𝐷⟶𝑁) → 𝐴:𝐷–1-1→ran 𝐴) |
70 | 69 | expcom 450 |
. 2
⊢ (𝐴:𝐷⟶𝑁 → (𝜑 → 𝐴:𝐷–1-1→ran 𝐴)) |
71 | 9, 70 | mpcom 37 |
1
⊢ (𝜑 → 𝐴:𝐷–1-1→ran 𝐴) |