Step |
Hyp |
Ref |
Expression |
1 |
|
frgrwopreg.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
frgrwopreg.d |
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) |
3 |
|
frgrwopreg.a |
⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } |
4 |
|
frgrwopreg.b |
⊢ 𝐵 = ( 𝑉 ∖ 𝐴 ) |
5 |
|
n0 |
⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |
6 |
3
|
rabeq2i |
⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) ) |
7 |
1
|
vdgfrgrgt2 |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑥 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
8 |
7
|
imp |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑥 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
9 |
|
breq2 |
⊢ ( 𝐾 = ( 𝐷 ‘ 𝑥 ) → ( 2 ≤ 𝐾 ↔ 2 ≤ ( 𝐷 ‘ 𝑥 ) ) ) |
10 |
2
|
fveq1i |
⊢ ( 𝐷 ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) |
11 |
10
|
breq2i |
⊢ ( 2 ≤ ( 𝐷 ‘ 𝑥 ) ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
12 |
9 11
|
bitrdi |
⊢ ( 𝐾 = ( 𝐷 ‘ 𝑥 ) → ( 2 ≤ 𝐾 ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
13 |
12
|
eqcoms |
⊢ ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → ( 2 ≤ 𝐾 ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
14 |
8 13
|
syl5ibrcom |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑥 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → 2 ≤ 𝐾 ) ) |
15 |
14
|
exp31 |
⊢ ( 𝐺 ∈ FriendGraph → ( 𝑥 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → 2 ≤ 𝐾 ) ) ) ) |
16 |
15
|
com14 |
⊢ ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → ( 𝑥 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) ) ) |
17 |
16
|
impcom |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) ) |
18 |
6 17
|
sylbi |
⊢ ( 𝑥 ∈ 𝐴 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) ) |
19 |
18
|
exlimiv |
⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) ) |
20 |
5 19
|
sylbi |
⊢ ( 𝐴 ≠ ∅ → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) ) |
21 |
20
|
3imp31 |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ≠ ∅ ) → 2 ≤ 𝐾 ) |