Step | Hyp | Ref
| Expression |
1 | | frgrancvvdeqlem9 26568 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
3 | | simpr 476 |
. . . . . . . 8
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
4 | 3 | imp 444 |
. . . . . . 7
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) |
5 | | frisusgra 26519 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
6 | 5 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) → 𝑉 USGrph 𝐸) |
7 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) → 𝑉 USGrph 𝐸) |
8 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
9 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) → 𝐸 ∈ Fin) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) → 𝐸 ∈ Fin) |
11 | 7, 8, 10 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
12 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
13 | | nbusgrafi 25977 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ Fin) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ Fin) |
15 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝑉 USGrph 𝐸) |
16 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑉 ∖ {𝑥}) → 𝑦 ∈ 𝑉) |
17 | 16 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝑦 ∈ 𝑉) |
18 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝐸 ∈ Fin) |
19 | 15, 17, 18 | 3jca 1235 |
. . . . . . . . . . 11
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
20 | | nbusgrafi 25977 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (〈𝑉, 𝐸〉 Neighbors 𝑦) ∈ Fin) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (〈𝑉, 𝐸〉 Neighbors 𝑦) ∈ Fin) |
22 | | hasheqf1o 12999 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ Fin ∧ (〈𝑉, 𝐸〉 Neighbors 𝑦) ∈ Fin) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) ↔ ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
23 | 14, 21, 22 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) ↔ ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) ↔ ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) ↔ ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
26 | 4, 25 | mpbird 246 |
. . . . . 6
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
27 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝑥 ∈ 𝑉) |
28 | 15, 27, 18 | 3jca 1235 |
. . . . . . . . 9
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
31 | | hashnbgravd 26439 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = ((𝑉 VDeg 𝐸)‘𝑥)) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = ((𝑉 VDeg 𝐸)‘𝑥)) |
33 | 19 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) → (𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
34 | 33 | adantr 480 |
. . . . . . 7
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
35 | | hashnbgravd 26439 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) = ((𝑉 VDeg 𝐸)‘𝑦)) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) = ((𝑉 VDeg 𝐸)‘𝑦)) |
37 | 26, 32, 36 | 3eqtr3d 2652 |
. . . . 5
⊢
((((((𝑉 FriendGrph
𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) |
38 | 37 | exp31 628 |
. . . 4
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → ((𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
39 | 38 | ralimdva 2945 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) ∧ 𝑥 ∈ 𝑉) → (∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
40 | 39 | ralimdva 2945 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
41 | 2, 40 | mpd 15 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦))) |