Step | Hyp | Ref
| Expression |
1 | | frgrancvvdeqlem9 26568 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
2 | | ovex 6577 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ V |
3 | | hasheqf1oi 13002 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ V → (∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)))) |
4 | 2, 3 | mp1i 13 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)))) |
5 | 4 | imim2d 55 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → ((𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦))))) |
6 | 5 | imp31 447 |
. . . . . 6
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
7 | | frisusgra 26519 |
. . . . . . . . . 10
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
8 | 7 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝑉 USGrph 𝐸) |
9 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝑥 ∈ 𝑉) |
10 | 8, 9 | jca 553 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉)) |
11 | 10 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉)) |
12 | | hashnbgravdg 26440 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑥 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = ((𝑉 VDeg 𝐸)‘𝑥)) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = ((𝑉 VDeg 𝐸)‘𝑥)) |
14 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑉 ∖ {𝑥}) → 𝑦 ∈ 𝑉) |
15 | 14 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → 𝑦 ∈ 𝑉) |
16 | 8, 15 | jca 553 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉)) |
17 | 16 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉)) |
18 | | hashnbgravdg 26440 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) = ((𝑉 VDeg 𝐸)‘𝑦)) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑦)) = ((𝑉 VDeg 𝐸)‘𝑦)) |
20 | 6, 13, 19 | 3eqtr3d 2652 |
. . . . 5
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)) |
21 | 20 | exp31 628 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → ((𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
22 | 21 | ralimdva 2945 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) → (∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
23 | 22 | ralimdva 2945 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦)))) |
24 | 1, 23 | mpd 15 |
1
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦))) |