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