Proof of Theorem vdgfrgragt2
Step | Hyp | Ref
| Expression |
1 | | vdgn0frgrav2 26551 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0)) |
2 | 1 | imp 444 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0) |
3 | | vdgn1frgrav2 26553 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1)) |
4 | 3 | imp 444 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1) |
5 | | frisusgra 26519 |
. . . . . . . . . 10
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
6 | | usgrav 25867 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
7 | 6 | simpld 474 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → 𝑉 ∈ V) |
8 | 5, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 ∈ V) |
9 | | usgrafun 25878 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
10 | 5, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝑉 FriendGrph 𝐸 → Fun 𝐸) |
11 | | funfn 5833 |
. . . . . . . . . 10
⊢ (Fun
𝐸 ↔ 𝐸 Fn dom 𝐸) |
12 | 10, 11 | sylib 207 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → 𝐸 Fn dom 𝐸) |
13 | 6 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
14 | 5, 13 | syl 17 |
. . . . . . . . . 10
⊢ (𝑉 FriendGrph 𝐸 → 𝐸 ∈ V) |
15 | | dmexg 6989 |
. . . . . . . . . 10
⊢ (𝐸 ∈ V → dom 𝐸 ∈ V) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → dom 𝐸 ∈ V) |
17 | 8, 12, 16 | 3jca 1235 |
. . . . . . . 8
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V)) |
18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V)) |
19 | | vdgrf 26425 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V) → (𝑉 VDeg 𝐸):𝑉⟶(ℕ0 ∪
{+∞})) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 VDeg 𝐸):𝑉⟶(ℕ0 ∪
{+∞})) |
21 | | simpr 476 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
22 | 20, 21 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ∈ (ℕ0 ∪
{+∞})) |
23 | | elun 3715 |
. . . . . 6
⊢ (((𝑉 VDeg 𝐸)‘𝑁) ∈ (ℕ0 ∪
{+∞}) ↔ (((𝑉
VDeg 𝐸)‘𝑁) ∈ ℕ0
∨ ((𝑉 VDeg 𝐸)‘𝑁) ∈ {+∞})) |
24 | | nn0n0n1ge2 11235 |
. . . . . . . 8
⊢ ((((𝑉 VDeg 𝐸)‘𝑁) ∈ ℕ0 ∧ ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 ∧ ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1) → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)) |
25 | 24 | 3exp 1256 |
. . . . . . 7
⊢ (((𝑉 VDeg 𝐸)‘𝑁) ∈ ℕ0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
26 | | elsni 4142 |
. . . . . . . 8
⊢ (((𝑉 VDeg 𝐸)‘𝑁) ∈ {+∞} → ((𝑉 VDeg 𝐸)‘𝑁) = +∞) |
27 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
28 | 27 | rexri 9976 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ* |
29 | | pnfge 11840 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ* → 2 ≤ +∞) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . 10
⊢ 2 ≤
+∞ |
31 | | breq2 4587 |
. . . . . . . . . 10
⊢ (((𝑉 VDeg 𝐸)‘𝑁) = +∞ → (2 ≤ ((𝑉 VDeg 𝐸)‘𝑁) ↔ 2 ≤ +∞)) |
32 | 30, 31 | mpbiri 247 |
. . . . . . . . 9
⊢ (((𝑉 VDeg 𝐸)‘𝑁) = +∞ → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)) |
33 | 32 | 2a1d 26 |
. . . . . . . 8
⊢ (((𝑉 VDeg 𝐸)‘𝑁) = +∞ → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
34 | 26, 33 | syl 17 |
. . . . . . 7
⊢ (((𝑉 VDeg 𝐸)‘𝑁) ∈ {+∞} → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
35 | 25, 34 | jaoi 393 |
. . . . . 6
⊢ ((((𝑉 VDeg 𝐸)‘𝑁) ∈ ℕ0 ∨ ((𝑉 VDeg 𝐸)‘𝑁) ∈ {+∞}) → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
36 | 23, 35 | sylbi 206 |
. . . . 5
⊢ (((𝑉 VDeg 𝐸)‘𝑁) ∈ (ℕ0 ∪
{+∞}) → (((𝑉
VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
37 | 22, 36 | syl 17 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
38 | 37 | adantr 480 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 0 → (((𝑉 VDeg 𝐸)‘𝑁) ≠ 1 → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)))) |
39 | 2, 4, 38 | mp2d 47 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 1 < (#‘𝑉)) → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁)) |
40 | 39 | ex 449 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁))) |