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 | | usgrafun 25878 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
11 | | funfn 5833 |
. . . . . . . . 9
⊢ (Fun
𝐸 ↔ 𝐸 Fn dom 𝐸) |
12 | 10, 11 | sylib 207 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → 𝐸 Fn dom 𝐸) |
13 | 1, 12 | syl 17 |
. . . . . . 7
⊢ (𝑉 FriendGrph 𝐸 → 𝐸 Fn dom 𝐸) |
14 | | 3cyclfrgrarn 26540 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) |
15 | | preq1 4212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑁 → {𝑎, 𝑏} = {𝑁, 𝑏}) |
16 | 15 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑁 → ({𝑎, 𝑏} ∈ ran 𝐸 ↔ {𝑁, 𝑏} ∈ ran 𝐸)) |
17 | | preq2 4213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑁 → {𝑐, 𝑎} = {𝑐, 𝑁}) |
18 | 17 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑁 → ({𝑐, 𝑎} ∈ ran 𝐸 ↔ {𝑐, 𝑁} ∈ ran 𝐸)) |
19 | 16, 18 | 3anbi13d 1393 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) ↔ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸))) |
20 | 19 | 2rexbidv 3039 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸))) |
21 | 20 | rspcva 3280 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) |
22 | | fvelrnb 6153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸 Fn dom 𝐸 → ({𝑁, 𝑏} ∈ ran 𝐸 ↔ ∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏})) |
23 | | prid1g 4239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑁, 𝑏}) |
24 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐸‘𝑥) = {𝑁, 𝑏} → (𝑁 ∈ (𝐸‘𝑥) ↔ 𝑁 ∈ {𝑁, 𝑏})) |
25 | 23, 24 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ 𝑉 → ((𝐸‘𝑥) = {𝑁, 𝑏} → 𝑁 ∈ (𝐸‘𝑥))) |
26 | 25 | reximdv 2999 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ 𝑉 → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))) |
27 | 26 | a1dd 48 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ 𝑉 → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} → (𝑏 ∈ 𝑉 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))) |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} → (𝑏 ∈ 𝑉 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
29 | 28 | com13 86 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑥 ∈ dom
𝐸(𝐸‘𝑥) = {𝑁, 𝑏} → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝑏 ∈ 𝑉 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
30 | 22, 29 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸 Fn dom 𝐸 → ({𝑁, 𝑏} ∈ ran 𝐸 → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝑏 ∈ 𝑉 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
31 | 30 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑁, 𝑏} ∈ ran 𝐸 → (𝐸 Fn dom 𝐸 → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝑏 ∈ 𝑉 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
32 | 31 | com25 97 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑁, 𝑏} ∈ ran 𝐸 → (𝑏 ∈ 𝑉 → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
33 | 32 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → (𝑏 ∈ 𝑉 → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
34 | 33 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ 𝑉 → (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
36 | 35 | rexlimivv 3018 |
. . . . . . . . . . . . . 14
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
37 | 21, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
38 | 37 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
39 | 38 | pm2.43a 52 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) → (𝐸 ∈ Fin → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
40 | 39 | com3l 87 |
. . . . . . . . . 10
⊢
(∀𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) → (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
41 | 14, 40 | syl 17 |
. . . . . . . . 9
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
42 | 41 | expcom 450 |
. . . . . . . 8
⊢ (1 <
(#‘𝑉) → (𝑉 FriendGrph 𝐸 → (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (𝐸 Fn dom 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
43 | 42 | com15 99 |
. . . . . . 7
⊢ (𝐸 Fn dom 𝐸 → (𝑉 FriendGrph 𝐸 → (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (1 < (#‘𝑉) → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)))))) |
44 | 13, 43 | mpcom 37 |
. . . . . 6
⊢ (𝑉 FriendGrph 𝐸 → (𝐸 ∈ Fin → (𝑁 ∈ 𝑉 → (1 < (#‘𝑉) → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))))) |
45 | 44 | 3imp1 1272 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
46 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑥 ∈ dom
𝐸 ¬ ¬ 𝑁 ∈ (𝐸‘𝑥) ↔ ¬ ∀𝑥 ∈ dom 𝐸 ¬ 𝑁 ∈ (𝐸‘𝑥)) |
47 | | notnotb 303 |
. . . . . . . 8
⊢ (𝑁 ∈ (𝐸‘𝑥) ↔ ¬ ¬ 𝑁 ∈ (𝐸‘𝑥)) |
48 | 47 | bicomi 213 |
. . . . . . 7
⊢ (¬
¬ 𝑁 ∈ (𝐸‘𝑥) ↔ 𝑁 ∈ (𝐸‘𝑥)) |
49 | 48 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑥 ∈ dom
𝐸 ¬ ¬ 𝑁 ∈ (𝐸‘𝑥) ↔ ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
50 | 46, 49 | bitr3i 265 |
. . . . 5
⊢ (¬
∀𝑥 ∈ dom 𝐸 ¬ 𝑁 ∈ (𝐸‘𝑥) ↔ ∃𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥)) |
51 | 45, 50 | sylibr 223 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ¬ ∀𝑥 ∈ dom 𝐸 ¬ 𝑁 ∈ (𝐸‘𝑥)) |
52 | | dmfi 8129 |
. . . . . . . . 9
⊢ (𝐸 ∈ Fin → dom 𝐸 ∈ Fin) |
53 | 52 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → dom 𝐸 ∈ Fin) |
54 | 53 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → dom 𝐸 ∈ Fin) |
55 | | rabexg 4739 |
. . . . . . 7
⊢ (dom
𝐸 ∈ Fin → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V) |
56 | | hasheq0 13015 |
. . . . . . 7
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ V → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 0 ↔ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = ∅)) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . 6
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 0 ↔ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = ∅)) |
58 | | rabeq0 3911 |
. . . . . 6
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} = ∅ ↔ ∀𝑥 ∈ dom 𝐸 ¬ 𝑁 ∈ (𝐸‘𝑥)) |
59 | 57, 58 | syl6bb 275 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = 0 ↔ ∀𝑥 ∈ dom 𝐸 ¬ 𝑁 ∈ (𝐸‘𝑥))) |
60 | 59 | necon3abid 2818 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≠ 0 ↔ ¬ ∀𝑥 ∈ dom 𝐸 ¬ 𝑁 ∈ (𝐸‘𝑥))) |
61 | 51, 60 | mpbird 246 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≠ 0) |
62 | 9, 61 | eqnetrd 2849 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0) |
63 | 62 | ex 449 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0)) |