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