Step | Hyp | Ref
| Expression |
1 | | frgrawopreg.a |
. . . 4
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} |
2 | | frgrawopreg.b |
. . . 4
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
3 | 1, 2 | frgrawopreglem3 26573 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏)) |
4 | | frgrancvvdgeq 26570 |
. . . 4
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦))) |
5 | | elrabi 3328 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} → 𝑎 ∈ 𝑉) |
6 | 5, 1 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉) |
7 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → {𝑥} = {𝑎}) |
8 | 7 | difeq2d 3690 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑉 ∖ {𝑥}) = (𝑉 ∖ {𝑎})) |
9 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝑎)) |
10 | | neleq2 2889 |
. . . . . . . . . . . 12
⊢
((〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝑎) → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↔ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↔ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎))) |
12 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑎)) |
13 | 12 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦) ↔ ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦))) |
14 | 11, 13 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) ↔ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
15 | 8, 14 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) ↔ ∀𝑦 ∈ (𝑉 ∖ {𝑎})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
16 | 15 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) → ∀𝑦 ∈ (𝑉 ∖ {𝑎})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
17 | 6, 16 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐴 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) → ∀𝑦 ∈ (𝑉 ∖ {𝑎})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) → ∀𝑦 ∈ (𝑉 ∖ {𝑎})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
19 | 2 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐵 ↔ 𝑏 ∈ (𝑉 ∖ 𝐴)) |
20 | | eldif 3550 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝑉 ∖ 𝐴) ↔ (𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴)) |
21 | 19, 20 | bitri 263 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴)) |
22 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴) ∧ 𝑎 ∈ 𝐴) → 𝑏 ∈ 𝑉) |
23 | | eleq1a 2683 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ 𝐴 → (𝑏 = 𝑎 → 𝑏 ∈ 𝐴)) |
24 | 23 | con3rr3 150 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑏 ∈ 𝐴 → (𝑎 ∈ 𝐴 → ¬ 𝑏 = 𝑎)) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴) → (𝑎 ∈ 𝐴 → ¬ 𝑏 = 𝑎)) |
26 | 25 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴) ∧ 𝑎 ∈ 𝐴) → ¬ 𝑏 = 𝑎) |
27 | | velsn 4141 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ {𝑎} ↔ 𝑏 = 𝑎) |
28 | 26, 27 | sylnibr 318 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴) ∧ 𝑎 ∈ 𝐴) → ¬ 𝑏 ∈ {𝑎}) |
29 | 22, 28 | eldifd 3551 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴) ∧ 𝑎 ∈ 𝐴) → 𝑏 ∈ (𝑉 ∖ {𝑎})) |
30 | 29 | ex 449 |
. . . . . . . . 9
⊢ ((𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴) → (𝑎 ∈ 𝐴 → 𝑏 ∈ (𝑉 ∖ {𝑎}))) |
31 | 21, 30 | sylbi 206 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → (𝑎 ∈ 𝐴 → 𝑏 ∈ (𝑉 ∖ {𝑎}))) |
32 | 31 | impcom 445 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ (𝑉 ∖ {𝑎})) |
33 | | neleq1 2888 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) ↔ 𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎))) |
34 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → ((𝑉 VDeg 𝐸)‘𝑦) = ((𝑉 VDeg 𝐸)‘𝑏)) |
35 | 34 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦) ↔ ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏))) |
36 | 33, 35 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ((𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)) ↔ (𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏)))) |
37 | 36 | rspcv 3278 |
. . . . . . 7
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → (∀𝑦 ∈ (𝑉 ∖ {𝑎})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)) → (𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏)))) |
38 | 32, 37 | syl 17 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑦 ∈ (𝑉 ∖ {𝑎})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑦)) → (𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏)))) |
39 | | nnel 2892 |
. . . . . . . . 9
⊢ (¬
𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) ↔ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎)) |
40 | | frisusgra 26519 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
41 | | nbgraeledg 25959 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎) ↔ {𝑏, 𝑎} ∈ ran 𝐸)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑉 FriendGrph 𝐸 → (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎) ↔ {𝑏, 𝑎} ∈ ran 𝐸)) |
43 | | prcom 4211 |
. . . . . . . . . . . . . . 15
⊢ {𝑏, 𝑎} = {𝑎, 𝑏} |
44 | 43 | eleq1i 2679 |
. . . . . . . . . . . . . 14
⊢ ({𝑏, 𝑎} ∈ ran 𝐸 ↔ {𝑎, 𝑏} ∈ ran 𝐸) |
45 | 42, 44 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢ (𝑉 FriendGrph 𝐸 → (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎) ↔ {𝑎, 𝑏} ∈ ran 𝐸)) |
46 | 45 | biimpa 500 |
. . . . . . . . . . . 12
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎)) → {𝑎, 𝑏} ∈ ran 𝐸) |
47 | 46 | a1d 25 |
. . . . . . . . . . 11
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎)) → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)) |
48 | 47 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸))) |
49 | 48 | a1d 25 |
. . . . . . . . 9
⊢ (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
50 | 39, 49 | sylbi 206 |
. . . . . . . 8
⊢ (¬
𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
51 | | eqneqall 2793 |
. . . . . . . . . 10
⊢ (((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏) → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)) |
52 | 51 | a1d 25 |
. . . . . . . . 9
⊢ (((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸))) |
53 | 52 | a1d 25 |
. . . . . . . 8
⊢ (((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
54 | 50, 53 | ja 172 |
. . . . . . 7
⊢ ((𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
55 | 54 | com12 32 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑎) → ((𝑉 VDeg 𝐸)‘𝑎) = ((𝑉 VDeg 𝐸)‘𝑏)) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
56 | 18, 38, 55 | 3syld 58 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) → (𝑉 FriendGrph 𝐸 → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
57 | 56 | com3l 87 |
. . . 4
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) → (𝑉 FriendGrph 𝐸 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸)))) |
58 | 4, 57 | mpcom 37 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝑉 VDeg 𝐸)‘𝑎) ≠ ((𝑉 VDeg 𝐸)‘𝑏) → {𝑎, 𝑏} ∈ ran 𝐸))) |
59 | 3, 58 | mpdi 44 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ ran 𝐸)) |
60 | 59 | ralrimivv 2953 |
1
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ ran 𝐸) |