Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . . . . 7
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | 1 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 𝑉 USGrph 𝐸) |
3 | | simp3 1056 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
4 | | simp2 1055 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 𝐸 ∈ Fin) |
5 | 2, 3, 4 | 3jca 1235 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
6 | 5 | adantr 480 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝐸 ∈ Fin)) |
7 | | vdusgraval 26434 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) |
8 | 7 | 3adant3 1074 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → ((𝑉 VDeg 𝐸)‘𝑁) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) |
9 | 6, 8 | syl 17 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) |
10 | | 3cyclfrgrarn2 26541 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
11 | 10 | 3ad2antl1 1216 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
12 | | preq1 4212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → {𝑎, 𝑏} = {𝑁, 𝑏}) |
13 | 12 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → ({𝑎, 𝑏} ∈ ran 𝐸 ↔ {𝑁, 𝑏} ∈ ran 𝐸)) |
14 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → {𝑐, 𝑎} = {𝑐, 𝑁}) |
15 | 14 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → ({𝑐, 𝑎} ∈ ran 𝐸 ↔ {𝑐, 𝑁} ∈ ran 𝐸)) |
16 | 13, 15 | 3anbi13d 1393 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑁 → (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) ↔ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸))) |
17 | 16 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑁 → ((𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) ↔ (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)))) |
18 | 17 | 2rexbidv 3039 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑁 → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)))) |
19 | 18 | rspcva 3280 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸))) |
20 | 1 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → 𝑉 USGrph 𝐸) |
21 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → 𝑁 ∈ 𝑉) |
22 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → 𝑏 ≠ 𝑐) |
23 | | 3simpb 1052 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) |
24 | 23 | ad3antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) |
25 | | usgra2edg1 25912 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
26 | 20, 21, 22, 24, 25 | syl31anc 1321 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
27 | 26 | 2a1d 26 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) ∧ 𝑉 FriendGrph 𝐸) → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))) |
28 | 27 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) ∧ 𝑁 ∈ 𝑉) → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
29 | 28 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))))) |
31 | 30 | rexlimivv 3018 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
32 | 19, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
33 | 32 | ex 449 |
. . . . . . . . 9
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))))) |
34 | 33 | pm2.43a 52 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (𝐸 ∈ Fin → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
35 | 34 | com25 97 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
36 | 35 | com13 86 |
. . . . . 6
⊢ (𝑉 FriendGrph 𝐸 → (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (1 < (#‘𝑉) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
37 | 36 | 3imp1 1272 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
38 | 11, 37 | mpd 15 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
39 | | dmfi 8129 |
. . . . . . . . . 10
⊢ (𝐸 ∈ Fin → dom 𝐸 ∈ Fin) |
40 | 39 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → dom 𝐸 ∈ Fin) |
41 | 40 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → dom 𝐸 ∈ Fin) |
42 | | rabexg 4739 |
. . . . . . . 8
⊢ (dom
𝐸 ∈ Fin → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V) |
43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V) |
44 | | hash1snb 13068 |
. . . . . . 7
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 1 ↔ ∃𝑖{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = {𝑖})) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 1 ↔ ∃𝑖{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = {𝑖})) |
46 | | reusn 4206 |
. . . . . 6
⊢
(∃!𝑥 ∈
dom 𝐸 𝑁 ∈ (𝐸‘𝑥) ↔ ∃𝑖{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = {𝑖}) |
47 | 45, 46 | syl6bbr 277 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 1 ↔ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
48 | 47 | necon3abid 2818 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≠ 1 ↔ ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
49 | 38, 48 | mpbird 246 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≠ 1) |
50 | 9, 49 | eqnetrd 2849 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1) |
51 | 50 | ex 449 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1)) |