Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . . . 6
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | 1 | anim1i 590 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) |
3 | 2 | adantr 480 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) |
4 | | vdusgraval 26434 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) |
6 | | 3cyclfrgrarn2 26541 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
7 | 6 | adantlr 747 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
8 | | preq1 4212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → {𝑎, 𝑏} = {𝑁, 𝑏}) |
9 | 8 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → ({𝑎, 𝑏} ∈ ran 𝐸 ↔ {𝑁, 𝑏} ∈ ran 𝐸)) |
10 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → {𝑐, 𝑎} = {𝑐, 𝑁}) |
11 | 10 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → ({𝑐, 𝑎} ∈ ran 𝐸 ↔ {𝑐, 𝑁} ∈ ran 𝐸)) |
12 | 9, 11 | 3anbi13d 1393 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑁 → (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) ↔ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸))) |
13 | 12 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑁 → ((𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) ↔ (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)))) |
14 | 13 | 2rexbidv 3039 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑁 → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)))) |
15 | 14 | rspcva 3280 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸))) |
16 | 1 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → 𝑉 USGrph 𝐸) |
17 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → 𝑁 ∈ 𝑉) |
18 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → 𝑏 ≠ 𝑐) |
19 | | 3simpb 1052 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) |
20 | 19 | ad3antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) |
21 | | usgra2edg1 25912 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
22 | 16, 17, 18, 20, 21 | syl31anc 1321 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
23 | 22 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
24 | 23 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))) |
25 | 24 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
26 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
27 | 26 | rexlimivv 3018 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
28 | 15, 27 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
29 | 28 | ex 449 |
. . . . . . . . 9
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
30 | 29 | pm2.43a 52 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
31 | 30 | com24 93 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑉 → (1 < (#‘𝑉) → (𝑉 FriendGrph 𝐸 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
32 | 31 | com3r 85 |
. . . . . 6
⊢ (𝑉 FriendGrph 𝐸 → (𝑁 ∈ 𝑉 → (1 < (#‘𝑉) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
33 | 32 | imp31 447 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
34 | 7, 33 | mpd 15 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
35 | | usgrav 25867 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
36 | 35 | simprd 478 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
37 | | dmexg 6989 |
. . . . . . . . . 10
⊢ (𝐸 ∈ V → dom 𝐸 ∈ V) |
38 | 1, 36, 37 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → dom 𝐸 ∈ V) |
39 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → dom 𝐸 ∈ V) |
40 | 39 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → dom 𝐸 ∈ V) |
41 | | rabexg 4739 |
. . . . . . 7
⊢ (dom
𝐸 ∈ V → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V) |
42 | | hash1snb 13068 |
. . . . . . 7
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 1 ↔ ∃𝑖{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = {𝑖})) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . 6
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 1 ↔ ∃𝑖{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = {𝑖})) |
44 | | reusn 4206 |
. . . . . 6
⊢
(∃!𝑥 ∈
dom 𝐸 𝑁 ∈ (𝐸‘𝑥) ↔ ∃𝑖{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = {𝑖}) |
45 | 43, 44 | syl6bbr 277 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 1 ↔ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
46 | 45 | necon3abid 2818 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≠ 1 ↔ ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
47 | 34, 46 | mpbird 246 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≠ 1) |
48 | 5, 47 | eqnetrd 2849 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1) |
49 | 48 | ex 449 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1)) |